diff -r 90ea835c07b3 -r f92963a33fe3 test/Tools/isac/Interpret/error-pattern.sml
--- a/test/Tools/isac/Interpret/error-pattern.sml	Sun Oct 09 06:53:03 2022 +0200
+++ b/test/Tools/isac/Interpret/error-pattern.sml	Sun Oct 09 07:44:22 2022 +0200
@@ -119,13 +119,13 @@
  val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
 		       ((#rules o Rule_Set.rep) Test_simplify)
 		       (sqrt_right false (@{theory "Pure"})) NONE 
-		       (TermC.str2term "x + 1 + - 1 * 2 = 0");
+		       (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0");
  (writeln o Derive.trtas2str) fod;
 
  val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
 		       ((#rules o Rule_Set.rep) Test_simplify)
 		       (sqrt_right false (@{theory "Pure"})) NONE 
-		       (TermC.str2term "- 2 * 1 + (1 + x) = 0");
+		       (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0");
  (writeln o Derive.trtas2str) ifod;
  fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
  val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
@@ -637,7 +637,7 @@
 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
-val t = TermC.str2term "Diff (x \<up> 2 + x + 1, x)";
+val t = TermC.parse_test @{context} "Diff (x \<up> 2 + x + 1, x)";
 case t of Const (\<^const_name>\<open>Diff\<close>, _) $ _ => ()
 	| _ => raise 
 	      error "diff.sml behav.changed for CAS Diff (..., x)";
@@ -902,11 +902,11 @@
 "--------- build fun check_for' ------------------------------";
 "--------- build fun check_for' ------------------------------";
 "--------- build fun check_for' ------------------------------";
-val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
+val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst;
 val rls = norm_Rational
 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
-val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
-val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2");
+val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4");
+val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "1 / 2");
 
 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
   rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
@@ -924,21 +924,21 @@
 norm_res = norm_inf;
 
 val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b";
-val (res, inf) = (TermC.str2term "(2 + 3)/2", TermC.str2term "3");
+val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/2", TermC.parse_test @{context} "3");
 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
 then () else error "error patt example1 changed";
 
 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
-val (res, inf) = (TermC.str2term "(2 + 3)/(2 + 4)", TermC.str2term "3 / 4");
+val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(2 + 4)", TermC.parse_test @{context} "3 / 4");
 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
 then () else error "error patt example2 changed";
 
 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
-val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
+val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4");
 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
 then () else error "error patt example3 changed";
 
-val inf =  TermC.str2term "1 / 2";
+val inf =  TermC.parse_test @{context} "1 / 2";
 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
 then () else error "error patt example3 changed";
 
@@ -946,15 +946,15 @@
 "--------- build fun check_for' ?bdv -------------------------";
 "--------- build fun check_for' ?bdv -------------------------";
 val ctxt = Proof_Context.init_global @{theory}
-val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst;
-val t = TermC.str2term "d_d x (x \<up> 2 + sin (x \<up> 4))";
+val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst;
+val t = TermC.parse_test @{context} "d_d x (x \<up> 2 + sin (x \<up> 4))";
 val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t;
 if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then ()
 else error "build fun check_for' ?bdv changed 1"; 
 
 val rls = norm_diff
 val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; 
-val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)");
+val (res, inf) = (TermC.parse_test @{context} "2 * x + d_d x (sin (x \<up> 4))", TermC.parse_test @{context} "2 * x + cos (4 * x \<up> 3)");
 
 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
   rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
@@ -984,11 +984,11 @@
 "--------- build fun check_for ------------------------";
 "--------- build fun check_for ------------------------";
 val (res, inf) =
-  (TermC.str2term "d_d x (x \<up> 2) + d_d x (sin (x \<up>  4))",
-   TermC.str2term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
+  (TermC.parse_test @{context} "d_d x (x \<up> 2) + d_d x (sin (x \<up>  4))",
+   TermC.parse_test @{context} "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
 val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]
 
-val env = [(TermC.str2term "v_v", TermC.str2term "x")];
+val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")];
 val errpats =
   [Error_Pattern.empty, (*generalised for testing*)
    ("chain-rule-diff-both",
@@ -1277,7 +1277,7 @@
 "--------- fun concat_deriv --------------------------------------";
 (*
  val ({rew_ord, erls, rules,...}, fo, ifo) = 
-     (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ - 1*2=0", TermC.str2term "-2*1+(x+1)=0");
+     (Rule_Set.rep Test_simplify, TermC.parse_test @{context} "x+1+ - 1*2=0", TermC.parse_test @{context} "-2*1+(x+1)=0");
  (tracing o Derive.trtas2str) fod';
 > ["
 (x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", "