1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue Jan 10 17:07:53 2023 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Jan 11 06:06:12 2023 +0100
     1.3 @@ -305,7 +305,7 @@
     1.4        |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
     1.5      val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
     1.6  
     1.7 -if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
     1.8 +if ThmC.string_of_thm ctxt eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
     1.9  
    1.10      val rhs = Thm.term_of (Thm.rhs_of eq);
    1.11      val _ = \<^assert> (is_num rhs);
    1.12 @@ -391,7 +391,7 @@
    1.13  val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "is_num");
    1.14  val t = @{term "9 is_num"};
    1.15  val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
    1.16 -if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
    1.17 +if str = "#is_num_9_" andalso ThmC.string_of_thm ctxt thm = "(9 is_num) = True"
    1.18  then () else error "adhoc_thm  9 is_num  changed";
    1.19  
    1.20  case get_calc_prog_id ctxt \<^const_name>\<open>less\<close> of
    1.21 @@ -401,7 +401,7 @@
    1.22  
    1.23  val t = @{term "4 < (4 :: real)"};
    1.24  val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
    1.25 -if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
    1.26 +if str = "#less_4_4" andalso ThmC.string_of_thm ctxt thm = "(4 < 4) = False"
    1.27  then () else error "adhoc_thm  4 < 4  changed";
    1.28  
    1.29  val SOME t = parseNEW @{context} "a < 4";
    1.30 @@ -411,13 +411,13 @@
    1.31  val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "PLUS");
    1.32  val SOME t = parseNEW @{context} "1 + (2::real)";
    1.33  val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
    1.34 -if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
    1.35 +if str = "#: 1 + 2 = 3" andalso ThmC.string_of_thm ctxt thm = "1 + 2 = 3"
    1.36  then () else error "adhoc_thm  1 + 2  changed";
    1.37  
    1.38  val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE");
    1.39  val t = @{term "6 / -8 :: real"};
    1.40  val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
    1.41 -if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
    1.42 +if str = "#divide_e6_~8" andalso ThmC.string_of_thm ctxt thm = "6 / - 8 = - 3 / 4"
    1.43  then () else error "adhoc_thm  6 / -8 = - 3 / 4  changed";
    1.44  
    1.45  case get_calc_prog_id ctxt "Prog_Expr.ident" of
    1.46 @@ -426,12 +426,12 @@
    1.47  
    1.48  val t = @{term "3 =!= (3 :: real)"};
    1.49  val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
    1.50 -if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
    1.51 +if str = "#ident_(3)_(3)" andalso ThmC.string_of_thm ctxt thm = "(3 =!= 3) = True"
    1.52  then () else error "adhoc_thm  (3 =!= 3)  changed";
    1.53  
    1.54  val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
    1.55  val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
    1.56 -if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
    1.57 +if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC.string_of_thm ctxt thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
    1.58  then () else error "adhoc_thm  (\<not> (4 + (4 * x + x ^ 2) =!= 0))  changed";
    1.59  
    1.60  "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";