diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -361,7 +361,7 @@
 
 val cancel_leading_coeff = prep_rls'(
   Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [], 
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>cancel_leading_coeff1\<close>,
@@ -384,7 +384,7 @@
 ML\<open>
 val complete_square = prep_rls'(
   Rule_Def.Repeat {id = "complete_square", preconds = [], 
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [],  errpatts = [],
     rules = [
       \<^rule_thm>\<open>complete_square1\<close>,
@@ -427,7 +427,7 @@
 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
 val d0_polyeq_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = PolyEq_erls,
     srls = Rule_Set.Empty, 
     calc = [], errpatts = [],
@@ -440,7 +440,7 @@
 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
 val d1_polyeq_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = PolyEq_erls,
     srls = Rule_Set.Empty, 
     calc = [], errpatts = [],
@@ -456,7 +456,7 @@
 (* isolate the bound variable in an d2 equation with bdv only;
   "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
 val d2_polyeq_bdv_only_simplify = prep_rls'(
-  Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+  Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
        \<^rule_thm>\<open>d2_prescind1\<close>, (*   ax+bx^2=0 -> x(a+bx)=0 *)
@@ -475,7 +475,7 @@
    'bdv' is a meta-constant*)
 val d2_polyeq_sq_only_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>d2_isolate_add1\<close>,(* a+   bx^2=0 -> bx^2=(-1)a*)
@@ -491,7 +491,7 @@
    'bdv' is a meta-constant*)
 val d2_polyeq_pqFormula_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
     srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>d2_pqformula1\<close>, (* q+px+ x^2=0 *)
@@ -518,7 +518,7 @@
    'bdv' is a meta-constant*)
 val d2_polyeq_abcFormula_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
     srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>d2_abcformula1\<close>, (*c+bx+cx^2=0 *)
@@ -545,7 +545,7 @@
    'bdv' is a meta-constant*)
 val d2_polyeq_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
     srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>d2_pqformula1\<close>, (* p+qx+ x^2=0 *)
@@ -578,7 +578,7 @@
 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
 val d3_polyeq_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
     srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>d3_reduce_equation1\<close>, (*a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0)*)
@@ -608,7 +608,7 @@
 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
 val d4_polyeq_simplify = prep_rls'(
   Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [],
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
     srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>d4_sub_u1\<close> (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)],
@@ -1128,7 +1128,7 @@
 ML\<open>
 val collect_bdv = prep_rls'(
   Rule_Def.Repeat{id = "collect_bdv", 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>bdv_collect_1\<close>,
@@ -1163,7 +1163,7 @@
    according to knowledge/Poly.sml.*) 
 val make_polynomial_in = prep_rls'(
   Rule_Set.Sequence {
-    id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       Rule.Rls_ expand_poly,
@@ -1189,7 +1189,7 @@
 ML\<open>
 val make_ratpoly_in = prep_rls'(
   Rule_Set.Sequence {
-    id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       Rule.Rls_ norm_Rational,