diff -r 90ea835c07b3 -r f92963a33fe3 test/Tools/isac/Knowledge/integrate.sml
--- a/test/Tools/isac/Knowledge/integrate.sml	Sun Oct 09 06:53:03 2022 +0200
+++ b/test/Tools/isac/Knowledge/integrate.sml	Sun Oct 09 07:44:22 2022 +0200
@@ -51,14 +51,14 @@
 "----------- parsing ------------------------------------";
 "----------- parsing ------------------------------------";
 "----------- parsing ------------------------------------";
-val t = TermC.str2term "Integral x D x";
-val t = TermC.str2term "Integral x \<up> 2 D x";
+val t = TermC.parse_test @{context} "Integral x D x";
+val t = TermC.parse_test @{context} "Integral x \<up> 2 D x";
 case t of 
     Const (\<^const_name>\<open>Integral\<close>, _) $
      (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
   | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
 
-val t = TermC.str2term "ff x is_f_x";
+val t = TermC.parse_test @{context} "ff x is_f_x";
 case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
 	| _ => error "integrate.sml: parsing: ff x is_f_x";
 
@@ -66,26 +66,26 @@
 "----------- integrate by rewriting ---------------------";
 "----------- integrate by rewriting ---------------------";
 "----------- integrate by rewriting ---------------------";
-val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
+val str = rewrit @{thm "integral_const"} (TermC.parse_test @{context} "Integral 1 D x");
 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
 
-val str = rewrit @{thm "integral_const"} (TermC.str2term  "Integral M'/EJ D x");
+val str = rewrit @{thm "integral_const"} (TermC.parse_test @{context}  "Integral M'/EJ D x");
 if term2s str = "M' / EJ * x" then ()
 else error "Integral M'/EJ D x   BY integral_const";
 
-val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
+val str = rewrit @{thm "integral_var"} (TermC.parse_test @{context} "Integral x D x");
 if term2s str = "x \<up> 2 / 2" then ()
 else error "Integral x D x   BY integral_var";
 
-val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
+val str = rewrit @{thm "integral_add"} (TermC.parse_test @{context} "Integral x + 1 D x");
 if term2s str = "Integral x D x + Integral 1 D x" then ()
 else error "Integral x + 1 D x   BY integral_add";
 
-val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
+val str = rewrit @{thm "integral_mult"} (TermC.parse_test @{context} "Integral M'/EJ * x \<up> 3 D x");
 if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
 else error "Integral M'/EJ * x \<up> 3 D x   BY integral_mult";
 
-val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
+val str = rewrit @{thm "integral_pow"} (TermC.parse_test @{context} "Integral x \<up> 3 D x");
 if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
 else error "integrate.sml Integral x \<up> 3 D x";
 
@@ -93,7 +93,7 @@
 "----------- test add_new_c, TermC.is_f_x ---------------------";
 "----------- test add_new_c, TermC.is_f_x ---------------------";
 "----------- test add_new_c, TermC.is_f_x ---------------------";
-val term = TermC.str2term "x \<up> 2 * c + c_2";
+val term = TermC.parse_test @{context} "x \<up> 2 * c + c_2";
 val cc = new_c term;
 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
 
@@ -108,7 +108,7 @@
 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
 
-val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
+val term = TermC.parse_test @{context} "ff x = x \<up> 2*c + c_2";
 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term;
 if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
@@ -173,9 +173,9 @@
 "----------- simplify by ruleset reducing make_ratpoly_in";
 val thy = @{theory "Isac_Knowledge"};
 val ctxt = Proof_Context.init_global thy;
-val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]; (*DOESN'T HELP*)
+val subst = [(TermC.parse_test @{context} "bdv ::real", TermC.parse_test @{context} "x ::real")]; (*DOESN'T HELP*)
 "===== test 1";
-val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
+val t = TermC.parse_test @{context} "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
 
 "----- stepwise from the rulesets in simplify_Integral and below-----";
 val rls = norm_Rational_noadd_fractions;
@@ -196,7 +196,7 @@
 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
 
 "===== test 4";
-val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
+val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];
 val rls = 
   (Rule_Set.append_rules "separate_bdv" collect_bdv
  	  [Thm ("separate_bdv", @{thm separate_bdv}),
@@ -221,7 +221,7 @@
 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
 
 "===== test 5";
-val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
+val t = TermC.parse_test @{context} "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
 val rls = simplify_Integral;
 val SOME (t,[]) = rewrite_set_inst_ ctxt true subs rls t;
 (* given was:   "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
@@ -231,10 +231,10 @@
 "........... 2nd integral ........................................";
 "........... 2nd integral ........................................";
 "........... 2nd integral ........................................";
-val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
+val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];
 
 val thy = @{theory Biegelinie};
-val t = TermC.str2term 
+val t = TermC.parse_test @{context} 
   "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
 
 val rls = simplify_Integral;
@@ -309,7 +309,7 @@
 "----------- rewrite 3rd integration in 7.27 ------------";
 "----------- rewrite 3rd integration in 7.27 ------------";
 "----------- rewrite 3rd integration in 7.27 ------------";
-val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
+val t = TermC.parse_test @{context} "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
 val SOME(t, _)= rewrite_set_inst_ ctxt true subs simplify_Integral t;
 if UnparseC.term t = 
   "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
@@ -358,7 +358,7 @@
 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
 
 val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _)) 
-	 $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
+	 $ Free ("ff", F3_type)) = TermC.parse_test @{context} "antiDerivativeName ff";
 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
 if F1_type = F3_type then () 
 else error "integrate.sml: unequal types in find's";