diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Poly.thy
--- a/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Poly.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -723,7 +723,7 @@
 \<close>
 ML \<open>
 val expand =
-  Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+  Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [
         \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
@@ -735,7 +735,7 @@
 ML \<open>
 (* erls for calculate_Rational + etc *)
 val powers_erls =
-  Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
       erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [
         \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
@@ -750,7 +750,7 @@
 
 \<close> ML \<open>
 val discard_minus =
-  Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+  Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [
         \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
@@ -759,7 +759,7 @@
 
 val expand_poly_ = 
   Rule_Def.Repeat{id = "expand_poly_", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = powers_erls, srls = Rule_Set.Empty,
       calc = [], errpatts = [],
       rules = [
@@ -785,7 +785,7 @@
 
 val expand_poly_rat_ = 
   Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls =  Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty [
         \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
         \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
@@ -813,7 +813,7 @@
 
 val simplify_power_ = 
   Rule_Def.Repeat{id = "simplify_power_", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Rule_Set.empty, srls = Rule_Set.Empty,
       calc = [], errpatts = [],
       rules = [
@@ -836,7 +836,7 @@
 
 val calc_add_mult_pow_ = 
   Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
       calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
 	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
@@ -851,7 +851,7 @@
 
 val reduce_012_mult_ = 
   Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Rule_Set.empty,srls = Rule_Set.Empty,
       calc = [], errpatts = [],
       rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
@@ -863,7 +863,7 @@
 
 val collect_numerals_ = 
   Rule_Def.Repeat{id = "collect_numerals_", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Atools_erls, srls = Rule_Set.Empty,
       calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
 	      ], errpatts = [],
@@ -884,7 +884,7 @@
 
 val reduce_012_ = 
   Rule_Def.Repeat{id = "reduce_012_", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [
         \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
@@ -904,7 +904,7 @@
 
 val expand_poly =
   Rule_Def.Repeat{id = "expand_poly", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [
         \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
@@ -925,7 +925,7 @@
 
 val simplify_power = 
   Rule_Def.Repeat{id = "simplify_power", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Rule_Set.empty, srls = Rule_Set.Empty,
       calc = [], errpatts = [],
       rules = [
@@ -941,7 +941,7 @@
 
 val collect_numerals = 
   Rule_Def.Repeat{id = "collect_numerals", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
       calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
 	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
@@ -959,7 +959,7 @@
       scr = Rule.Empty_Prog};
 val reduce_012 = 
   Rule_Def.Repeat{id = "reduce_012", preconds = [], 
-      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+      rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Rule_Set.append_rules "erls_in_reduce_012" Rule_Set.empty [
         \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
         \<^rule_thm>\<open>not_false\<close>,
@@ -989,7 +989,7 @@
   (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
 val order_add_mult = 
   Rule_Def.Repeat{id = "order_add_mult", preconds = [], 
-      rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
+      rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
       erls = Rule_Set.empty,srls = Rule_Set.Empty,
       calc = [], errpatts = [],
       rules = [
@@ -1029,7 +1029,7 @@
              which evaluates (the instantiated) "?p is_multUnordered" to true *)
 	  [([TermC.parse_patt \<^theory> "?p is_multUnordered"], 
              TermC.parse_patt \<^theory> "?p :: real")],
-	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+	  rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
 	  erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
 			    [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
 	  calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
@@ -1044,7 +1044,7 @@
 		     attach_form = attach_form}};
 val order_mult_rls_ = 
   Rule_Def.Repeat {id = "order_mult_rls_", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Rule_Set.empty,srls = Rule_Set.Empty,
     calc = [], errpatts = [],
     rules = [
@@ -1069,7 +1069,7 @@
 	      TermC.parse_patt @{theory} "?p :: real" 
 	    (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment 
 	      fuer die Evaluation der Precondition "p is_addUnordered"*))],
-	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+	  rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
 	  erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
 			[\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
 	  calc = [
@@ -1087,7 +1087,7 @@
 
 val order_add_rls_ =
   Rule_Def.Repeat {id = "order_add_rls_", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Rule_Set.empty, srls = Rule_Set.Empty,
     calc = [], errpatts = [],
     rules = [
@@ -1108,7 +1108,7 @@
 val make_polynomial(*MG.03, overwrites version from above, 
     previously 'make_polynomial_'*) =
   Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list, 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
     rules = [
        Rule.Rls_ discard_minus,
@@ -1127,7 +1127,7 @@
 ML \<open>
 val norm_Poly(*=make_polynomial*) = 
   Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list, 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
        Rule.Rls_ discard_minus,
@@ -1149,7 +1149,7 @@
 (* MG necessary  for termination of norm_Rational(*_mg*) in Rational.ML*)
 val make_rat_poly_with_parentheses =
   Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list, 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       Rule.Rls_ discard_minus,
@@ -1375,5 +1375,5 @@
   Find: "normalform n_n"
 ML \<open>
 \<close> ML \<open>
-\<close> 
+\<close>
 end