diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/eqsystem-2.sml
--- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -207,9 +207,9 @@
   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
   "0 = c_4, " ^
   "0 = c_3]");
-val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
-val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
-val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
+val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
+val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
+val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
 if UnparseC.term t = 
   "[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]"
 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";