diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
index 4a27a3c18..6681fb9ac 100644
--- a/test/lean/bitfield.expected.lean
+++ b/test/lean/bitfield.expected.lean
@@ -5,7 +5,7 @@ structure cr_type  where
 
 
 def undefined_cr_type (lit : Unit) : cr_type :=
-  sorry /- internal_plet -/
+  sorry
 
 def Mk_cr_type (v : BitVec 8) : cr_type :=
   {bits := v}
@@ -17,7 +17,7 @@ def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)}
 
 def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit :=
-  sorry /- internal_plet -/
+  sorry
 
 def _get_cr_type_CR0 (v : cr_type) : BitVec 4 :=
   (Sail.BitVec.extractLsb v.bits 7 4)
@@ -26,7 +26,7 @@ def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)}
 
 def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit :=
-  sorry /- internal_plet -/
+  sorry
 
 def _get_cr_type_CR1 (v : cr_type) : BitVec 2 :=
   (Sail.BitVec.extractLsb v.bits 3 2)
@@ -35,7 +35,7 @@ def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)}
 
 def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit :=
-  sorry /- internal_plet -/
+  sorry
 
 def _get_cr_type_CR3 (v : cr_type) : BitVec 2 :=
   (Sail.BitVec.extractLsb v.bits 1 0)
@@ -44,7 +44,7 @@ def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)}
 
 def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit :=
-  sorry /- internal_plet -/
+  sorry
 
 def _get_cr_type_GT (v : cr_type) : BitVec 1 :=
   (Sail.BitVec.extractLsb v.bits 6 6)
@@ -53,7 +53,7 @@ def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)}
 
 def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit :=
-  sorry /- internal_plet -/
+  sorry
 
 def _get_cr_type_LT (v : cr_type) : BitVec 1 :=
   (Sail.BitVec.extractLsb v.bits 7 7)
@@ -62,7 +62,7 @@ def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)}
 
 def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit :=
-  sorry /- internal_plet -/
+  sorry
 
 def initialize_registers : Unit :=
   ()