diff --git a/examples/arm_cm0/balrob/balrob_endsScript.sml b/examples/arm_cm0/balrob/balrob_endsScript.sml
index d5ab722f1..e1b8b9d2c 100644
--- a/examples/arm_cm0/balrob/balrob_endsScript.sml
+++ b/examples/arm_cm0/balrob/balrob_endsScript.sml
@@ -11,7 +11,18 @@ val locs =
    0x100013dc);
 
 val symb_exec_thm = birs_summary birs_prog_config reqs locs;
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
 
-Theorem balrob_clzsi2_symb_exec_thm = symb_exec_thm
+(* ------------------------------------ *)
+val entry_name = "__lesf2";
+val reqs = get_fun_usage entry_name;
+val locs =
+  (0x10000a4c,
+   0x10000ad2);
+
+val symb_exec_thm = birs_summary birs_prog_config reqs locs;
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
+
+(* ------------------------------------ *)
 
 val _ = export_theory ();
diff --git a/examples/arm_cm0/balrob/balrob_insttestScript.sml b/examples/arm_cm0/balrob/balrob_insttestScript.sml
index 83ee5c5d7..d6ca34df7 100644
--- a/examples/arm_cm0/balrob/balrob_insttestScript.sml
+++ b/examples/arm_cm0/balrob/balrob_insttestScript.sml
@@ -10,7 +10,7 @@ open balrob_endsTheory;
 
 val _ = new_theory "balrob_insttest";
 
-(* instantiation test *)
+(* insttest *)
 val reqs = (0,63);
 val locs =
   (0x100012d6,
@@ -18,12 +18,12 @@ val locs =
 
 val symb_exec_thm = birs_summary birs_prog_config reqs locs;
 
-Theorem balrob_insttest_symb_exec_thm = symb_exec_thm
+Theorem balrob_summary_insttest_thm = symb_exec_thm
 
 
 (* now instantiate *)
-val A_thm = balrob_insttest_symb_exec_thm;
-val B_thm = balrob_clzsi2_symb_exec_thm;
+val A_thm = balrob_summary_insttest_thm;
+val B_thm = balrob_summary___clzsi2_thm;
 val inst_thm = birs_basic_instantiate birs_prog_config A_thm B_thm;
 
 Theorem balrob_insttest_symb_inst_thm = inst_thm
diff --git a/examples/arm_cm0/balrob/balrob_symb_transfScript.sml b/examples/arm_cm0/balrob/balrob_symb_transfScript.sml
index ca5222fb7..df2f8bd44 100644
--- a/examples/arm_cm0/balrob/balrob_symb_transfScript.sml
+++ b/examples/arm_cm0/balrob/balrob_symb_transfScript.sml
@@ -15,7 +15,7 @@ open balrob_endsTheory;
 val _ = new_theory "balrob_symb_transf";
 
 
-val balrob_exec_thm = balrob_clzsi2_symb_exec_thm;
+val balrob_exec_thm = balrob_summary___clzsi2_thm;
 
 (**)
 val bprog_envtyl_tm = (fst o dest_eq o concl) balrob_birenvtyl_def;