diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/Knowledge/eqsystem-1.sml
--- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Nov 16 10:30:59 2022 +0100
+++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Nov 16 17:42:41 2022 +0100
@@ -124,28 +124,28 @@
 "----------- rewrite-order ord_simplify_System -------------------";
 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
-if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
+if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
 				       TermC.parse_test @{context}"c * x") then ()
 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
 
-if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
+if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
 				       TermC.parse_test @{context}"c_2") then ()
 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
 
-if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x", 
+if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"c * x", 
 				       TermC.parse_test @{context}"c_2") then ()
 else error "integrate.sml, (c * x) < (c_2) not#3";
 
 "--- mult.commute ---";
-if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c", 
+if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"x * c", 
 				       TermC.parse_test @{context}"c * x") then ()
 else error "integrate.sml, (x * c) < (c * x) not#4";
 
-if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
+if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
 				       TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)") 
 then () else error "integrate.sml, (. * .) < (. * .) not#5";
 
-if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
+if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
 				       TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)") 
 then () else error "integrate.sml, (. * .) < (. * .) not#6";
 
@@ -240,7 +240,7 @@
 else error "eqsystem.sml top_down_substitution,2x2] order_system";
 
 if not (ord_simplify_System
-	    false thy [] 
+	    false ctxt [] 
 	    (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", 
 	     TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) 
 then () else error "eqsystem.sml, order_result rew_ord";