1.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -207,9 +207,9 @@
     1.4    "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
     1.5    "0 = c_4, " ^
     1.6    "0 = c_3]");
     1.7 -val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
     1.8 -val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
     1.9 -val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
    1.10 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
    1.11 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
    1.12 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
    1.13  if UnparseC.term t = 
    1.14    "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
    1.15  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";