diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/PolyMinus.thy
--- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -191,7 +191,7 @@
 
 val ordne_alphabetisch = 
   Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [],
     erls = erls_ordne_alphabetisch, 
     rules = [
       \<^rule_thm>\<open>tausche_plus\<close>, (*"b kleiner a ==> (b + a) = (a + b)"*)
@@ -206,7 +206,7 @@
 
 val fasse_zusammen = 
   Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], 
-	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+	  rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
 	  erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty 
 	  	[\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")],
 	  srls = Rule_Set.Empty, calc = [], errpatts = [],
@@ -248,7 +248,7 @@
     
 val verschoenere = 
   Rule_Def.Repeat{id = "verschoenere", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [],
     erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty 
 		  [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
     rules = [
@@ -268,7 +268,7 @@
 
 val klammern_aufloesen = 
   Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, 
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, 
     calc = [], errpatts = [], erls = Rule_Set.Empty, 
     rules = [
       \<^rule_thm_sym>\<open>add.assoc\<close>, (*"a + (b + c) = (a + b) + c"*)
@@ -279,7 +279,7 @@
 
 val klammern_ausmultiplizieren = 
   Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, 
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, 
     calc = [], errpatts = [], erls = Rule_Set.Empty, 
     rules = [
       \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
@@ -291,7 +291,7 @@
 
 val ordne_monome = 
   Rule_Def.Repeat {
-    id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+    id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     srls = Rule_Set.Empty, calc = [], errpatts = [], 
     erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [
       \<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),