1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Nov 16 10:30:59 2022 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Nov 16 17:42:41 2022 +0100
     1.3 @@ -124,28 +124,28 @@
     1.4  "----------- rewrite-order ord_simplify_System -------------------";
     1.5  "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
     1.6  "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
     1.7 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
     1.8 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
     1.9  				       TermC.parse_test @{context}"c * x") then ()
    1.10  else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
    1.11  
    1.12 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
    1.13 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
    1.14  				       TermC.parse_test @{context}"c_2") then ()
    1.15  else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
    1.16  
    1.17 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x", 
    1.18 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"c * x", 
    1.19  				       TermC.parse_test @{context}"c_2") then ()
    1.20  else error "integrate.sml, (c * x) < (c_2) not#3";
    1.21  
    1.22  "--- mult.commute ---";
    1.23 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c", 
    1.24 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"x * c", 
    1.25  				       TermC.parse_test @{context}"c * x") then ()
    1.26  else error "integrate.sml, (x * c) < (c * x) not#4";
    1.27  
    1.28 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
    1.29 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
    1.30  				       TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)") 
    1.31  then () else error "integrate.sml, (. * .) < (. * .) not#5";
    1.32  
    1.33 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
    1.34 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
    1.35  				       TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)") 
    1.36  then () else error "integrate.sml, (. * .) < (. * .) not#6";
    1.37  
    1.38 @@ -240,7 +240,7 @@
    1.39  else error "eqsystem.sml top_down_substitution,2x2] order_system";
    1.40  
    1.41  if not (ord_simplify_System
    1.42 -	    false thy [] 
    1.43 +	    false ctxt [] 
    1.44  	    (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", 
    1.45  	     TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) 
    1.46  then () else error "eqsystem.sml, order_result rew_ord";