diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -257,7 +257,7 @@
   | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
 
 "======= compare tausche_plus with real_num_collect";
-val od = dummy_ord;
+val od = Rewrite_Ord.function_empty;
 
 val erls = erls_ordne_alphabetisch;
 val t = TermC.str2term "b + a";
@@ -526,12 +526,12 @@
 val erls = erls_ordne_alphabetisch;
 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 val SOME (t',_) = 
-    rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus} t;
+    rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus} t;
 UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
 
 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 val NONE = 
-    rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus_plus} t;
+    rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus_plus} t;
 
 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 val SOME (t',_) =