diff --git a/examples/arm_cm0/balrob/balrob_faddScript.sml b/examples/arm_cm0/balrob/balrob_faddScript.sml
index 7998166f2..bed8af94f 100644
--- a/examples/arm_cm0/balrob/balrob_faddScript.sml
+++ b/examples/arm_cm0/balrob/balrob_faddScript.sml
@@ -49,7 +49,7 @@ val balrob_summary___aeabi_fadd_c3_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 val entry_name = "__aeabi_fadd";
 val reqs = get_fun_usage entry_name;
 val locs =
@@ -64,7 +64,7 @@ val symb_exec_thm = birs_summary birs_prog_config
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 
diff --git a/examples/arm_cm0/balrob/balrob_fdivScript.sml b/examples/arm_cm0/balrob/balrob_fdivScript.sml
index 55c0f27af..5868165ec 100644
--- a/examples/arm_cm0/balrob/balrob_fdivScript.sml
+++ b/examples/arm_cm0/balrob/balrob_fdivScript.sml
@@ -106,7 +106,7 @@ val balrob_summary___aeabi_fdiv_c7_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 (* TODO: uses two jump table encoded in manually extracted cfg! *)
 (* TODO: loads constants from memory! *)
 val entry_name = "__aeabi_fdiv";
@@ -132,7 +132,7 @@ val symb_exec_thm = birs_summary_gen
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 
diff --git a/examples/arm_cm0/balrob/balrob_fmulScript.sml b/examples/arm_cm0/balrob/balrob_fmulScript.sml
index c827ad9e7..2b6dc18e5 100644
--- a/examples/arm_cm0/balrob/balrob_fmulScript.sml
+++ b/examples/arm_cm0/balrob/balrob_fmulScript.sml
@@ -94,7 +94,7 @@ val balrob_summary___aeabi_fmul_c8_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 (* TODO: uses one jump table encoded in manually extracted cfg! used to take 3 times as much time as sub or div *)
 (* TODO: loads constants from memory! is the constant loading part of the lifting? better add some code to check this *)
 val entry_name = "__aeabi_fmul";
@@ -118,7 +118,7 @@ val symb_exec_thm = birs_summary_gen
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 
diff --git a/examples/arm_cm0/balrob/balrob_fsubScript.sml b/examples/arm_cm0/balrob/balrob_fsubScript.sml
index 5c1141bae..b0a00983f 100644
--- a/examples/arm_cm0/balrob/balrob_fsubScript.sml
+++ b/examples/arm_cm0/balrob/balrob_fsubScript.sml
@@ -104,7 +104,7 @@ val balrob_summary___aeabi_fsub_c8_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 val entry_name = "__aeabi_fsub";
 val reqs = get_fun_usage entry_name;
 val locs =
@@ -124,7 +124,7 @@ val symb_exec_thm = birs_summary birs_prog_config
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 
diff --git a/examples/arm_cm0/balrob/balrob_ftopScript.sml b/examples/arm_cm0/balrob/balrob_ftopScript.sml
index 54f5a635e..7a1159ccc 100644
--- a/examples/arm_cm0/balrob/balrob_ftopScript.sml
+++ b/examples/arm_cm0/balrob/balrob_ftopScript.sml
@@ -4,16 +4,16 @@ open balrob_supportLib;
 
 open balrob_endsTheory;
 open balrob_miscTheory;
+(*
 open balrob_fadd_fakeTheory;
 open balrob_fsub_fakeTheory;
 open balrob_fmul_fakeTheory;
 open balrob_fdiv_fakeTheory;
-(*
+*)
 open balrob_faddTheory;
 open balrob_fsubTheory;
 open balrob_fmulTheory;
 open balrob_fdivTheory;
-*)
 
 val _ = new_theory "balrob_ftop";
 
diff --git a/examples/arm_cm0/balrob/balrob_topScript.sml b/examples/arm_cm0/balrob/balrob_topScript.sml
index 64309fa8f..28f855a69 100644
--- a/examples/arm_cm0/balrob/balrob_topScript.sml
+++ b/examples/arm_cm0/balrob/balrob_topScript.sml
@@ -4,10 +4,16 @@ open balrob_supportLib;
 
 open balrob_endsTheory;
 open balrob_miscTheory;
+(*
 open balrob_fadd_fakeTheory;
 open balrob_fsub_fakeTheory;
 open balrob_fmul_fakeTheory;
 open balrob_fdiv_fakeTheory;
+*)
+open balrob_faddTheory;
+open balrob_fsubTheory;
+open balrob_fmulTheory;
+open balrob_fdivTheory;
 open balrob_ftopTheory;
 
 val _ = new_theory "balrob_top";
@@ -24,12 +30,6 @@ val locs =
   ( 0x10001504,
    [0x100016e0]);
 
-(*
-val locs =
-  ( 0x10001504,
-   [0x1000151a]);
-*)
-
 val symb_exec_thm = birs_summary_gen
   (fn x => ((*print "\n\n"; print_term x; print "\n\n";*) birs_simpLib.birs_simp_ID_fun x))
   (const_load_32_32_cheat_thms_fromprog_range (0x100016e4, 0x10001a88))