diff -r d2407e9cb491 -r 59a3af532717 test/Tools/isac/ProgLang/evaluate.sml
--- a/test/Tools/isac/ProgLang/evaluate.sml	Thu Jul 28 11:43:27 2022 +0200
+++ b/test/Tools/isac/ProgLang/evaluate.sml	Sat Jul 30 16:47:45 2022 +0200
@@ -48,6 +48,7 @@
 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
 val t = TermC.str2term "((1+2)*4/3) \<up> 2";
 val thy = @{theory};
+val ctxt = Proof_Context.init_global @{theory}
 val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
 val plus =   ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
@@ -55,22 +56,22 @@
 
 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
-val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_  1 + 2 = 3  changed";
 
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
-val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t'', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_  3 * 4 = 12  changed";
 
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
-val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_  12 / 3 = 4  changed";
 
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
-val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t'''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
 if UnparseC.term t'''' = "16" then () else error "calculate_  12 / 3 = 4  changed";
 
 "----------- calculate from Prog --------------------------------- -----------------------------";
@@ -121,7 +122,7 @@
  val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
  val ct = @{term
    "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
-case calculate_ thy op_ ct of
+case calculate_ ctxt op_ ct of
   SOME _ => ()
 | NONE => error "calculate_ test-root-equ changed";
 (*
@@ -134,13 +135,13 @@
  val ctxt = (ThyC.id_to_ctxt "Test")
  val t = TermC.parseNEW' ctxt "6 / 2";
  val rls = Test_simplify;
- val (t,_) = the (rewrite_set_ thy false rls t);
+ val (t,_) = the (rewrite_set_ ctxt false rls t);
 (*val t = Free ("3", "Real.real") : term*)
 
 (*--------------(3): is_num works ?: -------------------------------------*)
  val t = TermC.parseNEW' ctxt "2 is_num";
  TermC.atomty t;
- rewrite_set_ @{theory Test} false tval_rls t;
+ rewrite_set_ ctxt false tval_rls t;
 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
 
  val t = TermC.str2term "2 * x is_num";
@@ -151,7 +152,6 @@
 "----------- check calculate bottom up ------------------";
 "----------- check calculate bottom up ------------------";
 (*-------------- eval_cancel works: *)
- Rewrite.trace_on := false; (*true false*)
  val thy = @{theory Test};
  val rls = Test_simplify;
  val t = TermC.parseNEW' ctxt "(-4) / 2";
@@ -160,21 +160,19 @@
 
 (*--------------(5): reproduce (1) with simpler term: ------------*)
  val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";
-case rewrite_set_ thy false rls t of
+case rewrite_set_ ctxt false rls t of
   SOME (t', []) =>
     if UnparseC.term t' = "4" then ()
     else error "rewrite_set_ (3+5)/2 changed 1"
 | _ => error "rewrite_set_ (3+5)/2 changed 2";
 
  val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";
-case rewrite_set_ thy false rls t of
+case rewrite_set_ ctxt false rls t of
   SOME (t', _) =>
     if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
 | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
 
- Rewrite.trace_on := false; (*true false*)
-
-(*--- Rewrite.trace_on before correction of ... --------------------
+(*--- trace_rewrite before correction of ... --------------------
  val ct = "(-3 + 2 * x + - 1) / 2";
  val (ct,_) = the (rewrite_set thy'  false rls ct);
 :
@@ -203,9 +201,8 @@
 
 
 (*===================*)
- Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
  val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";
-val SOME (res, []) = rewrite_set_ thy false rls t;
+val SOME (res, []) = rewrite_set_ ctxt false rls t;
 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_  x + (- 1 + -3) / 2  changed";
 "x + (-4) / 2";						
 (*
@@ -221,8 +218,6 @@
 ### trying calc. 'pow'
 *)
 
- Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
-
 " ================= evaluate.sml: calculate_ 2002 =================== ";
 " ================= evaluate.sml: calculate_ 2002 =================== ";
 " ================= evaluate.sml: calculate_ 2002 =================== ";
@@ -230,33 +225,33 @@
 val thy = @{theory Test};
  val t = TermC.parseNEW' ctxt "12 / 3";
 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
-val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 "12 / 3 = 4";
 val thy = @{theory Test};
  val t = TermC.parseNEW' ctxt "4 \<up> 2";
 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
-val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
 "4 ^ 2 = 16";
 
  val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
 "1 + 2 = 3";
- val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+ val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
  UnparseC.term t;
 "(3 * 4 / 3) \<up> 2";
  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
 "3 * 4 = 12";
- val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+ val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
  UnparseC.term t;
 "(12 / 3) \<up> 2";
  val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
 "12 / 3 = 4";
- val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+ val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
  UnparseC.term t;
 "4 \<up> 2";
  val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
 "4 \<up> 2 = 16";
- val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
+ val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
  UnparseC.term t;
 "16";
  if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
@@ -342,7 +337,7 @@
 if UnparseC.term t' = "(2 * x is_num) = False" then ()
 else error "is_num 2 * x is_num CHANGED";
 
-val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
+val SOME (t',_) = rewrite_set_ ctxt false tval_rls t;
 if UnparseC.term t' = "False" then ()
 else error "rewrite_set_ 2 * x is_num CHANGED";