1.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Sun Sep 12 15:40:15 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Sun Sep 12 15:53:36 2021 +0200
     1.3 @@ -226,15 +226,13 @@
     1.4  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
     1.5  
     1.6  val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
     1.7 -if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
     1.8 -  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"*)
     1.9 -  "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
    1.10 +if UnparseC.term t =
    1.11 +  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
    1.12  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
    1.13  
    1.14  val SOME (t, _) = rewrite_set_ thy false order_system t;
    1.15 -if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
    1.16 -  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"*)
    1.17 -  "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
    1.18 +if UnparseC.term t =
    1.19 +  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
    1.20  then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
    1.21  
    1.22  "----- 7.70 with met normalise: ";