1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -116,13 +116,13 @@
     1.4     *)
     1.5  "----------------------------------------------------------";
     1.6  
     1.7 - val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls 
     1.8 + val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
     1.9  		       ((#rules o Rule_Set.rep) Test_simplify)
    1.10  		       (sqrt_right false (@{theory "Pure"})) NONE 
    1.11  		       (TermC.str2term "x + 1 + - 1 * 2 = 0");
    1.12   (writeln o Derive.trtas2str) fod;
    1.13  
    1.14 - val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls 
    1.15 + val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
    1.16  		       ((#rules o Rule_Set.rep) Test_simplify)
    1.17  		       (sqrt_right false (@{theory "Pure"})) NONE 
    1.18  		       (TermC.str2term "- 2 * 1 + (1 + x) = 0");
    1.19 @@ -909,14 +909,14 @@
    1.20  val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2");
    1.21  
    1.22  val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
    1.23 -  rew_sub thy 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.24 +  rew_sub ctxt 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.25  if rewritten then NONE else SOME "e_errpatID";
    1.26  
    1.27 -val norm_res = case rewrite_set_ (Isac()) false rls res' of
    1.28 +val norm_res = case rewrite_set_ ctxt false rls res' of
    1.29    NONE => res'
    1.30  | SOME (norm_res, _) => norm_res
    1.31  
    1.32 -val norm_inf = case rewrite_set_ (Isac()) false rls inf of
    1.33 +val norm_inf = case rewrite_set_ ctxt false rls inf of
    1.34    NONE => inf
    1.35  | SOME (norm_inf, _) => norm_inf;
    1.36  
    1.37 @@ -945,9 +945,10 @@
    1.38  "--------- build fun check_for' ?bdv -------------------------";
    1.39  "--------- build fun check_for' ?bdv -------------------------";
    1.40  "--------- build fun check_for' ?bdv -------------------------";
    1.41 +val ctxt = Proof_Context.init_global @{theory}
    1.42  val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
    1.43  val t = TermC.str2term "d_d x (x \<up> 2 + sin (x \<up> 4))";
    1.44 -val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
    1.45 +val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t;
    1.46  if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then ()
    1.47  else error "build fun check_for' ?bdv changed 1"; 
    1.48  
    1.49 @@ -956,17 +957,17 @@
    1.50  val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)");
    1.51  
    1.52  val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
    1.53 -  rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.54 +  rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.55  if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
    1.56  else error "build fun check_for' ?bdv changed 2";
    1.57  
    1.58 -val norm_res = case rewrite_set_inst_ (Isac()) false subst rls  res' of
    1.59 +val norm_res = case rewrite_set_inst_ ctxt false subst rls  res' of
    1.60    NONE => res'
    1.61  | SOME (norm_res, _) => norm_res;
    1.62  if UnparseC.term norm_res = "2 * x + cos (4 * x \<up> 3)" then ()
    1.63  else error "build fun check_for' ?bdv changed 3";
    1.64  
    1.65 -val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
    1.66 +val norm_inf = case rewrite_set_inst_ ctxt false subst rls inf of
    1.67    NONE => inf
    1.68  | SOME (norm_inf, _) => norm_inf;
    1.69  if UnparseC.term norm_inf = "2 * x + cos (4 * x \<up> 3)" then ()
    1.70 @@ -1118,7 +1119,7 @@
    1.71    val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
    1.72    (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
    1.73  val (form', _, _, rewritten) =
    1.74 -      rew_sub (Isac()) 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.75 +      rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.76  
    1.77  if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then ()
    1.78  else error "find_fill_patterns changed 3";