diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -190,7 +190,7 @@
   #2 NOT using common_nominator_p                          .*)
 val norm_System_noadd_fractions = 
   Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [(*sequence given by operator precedence*)
   		Rule.Rls_ discard_minus,
@@ -209,7 +209,7 @@
   *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
 val norm_System = 
   Rule_Def.Repeat {id = "norm_System", preconds = [], 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [(*sequence given by operator precedence*)
   		Rule.Rls_ discard_minus,
@@ -235,7 +235,7 @@
    analoguous to simplify_Integral                                       .*)
 val simplify_System_parenthesized = 
   Rule_Set.Sequence {id = "simplify_System_parenthesized", 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_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
@@ -255,7 +255,7 @@
 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
 val simplify_System = 
   Rule_Set.Sequence {id = "simplify_System", 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_ norm_Rational,
@@ -274,7 +274,7 @@
 ML \<open>
 val isolate_bdvs = 
   Rule_Def.Repeat {
-    id="isolate_bdvs", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
+    id="isolate_bdvs", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
     erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [
       (\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))], 
     srls = Rule_Set.Empty, calc = [], errpatts = [],
@@ -287,7 +287,7 @@
 ML \<open>
 val isolate_bdvs_4x4 = 
   Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [], 
-    rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
+    rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
     erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [
       \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
       \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
@@ -318,9 +318,9 @@
 
 val prls_triangular = 
   Rule_Def.Repeat {
-    id="prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
+    id="prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
     erls = Rule_Def.Repeat {
-      id="erls_prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
+      id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
       erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [(*for precond NTH_CONS ...*)
          \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
@@ -344,9 +344,9 @@
  more similarity to prls_triangular desirable*)
 val prls_triangular4 = 
   Rule_Def.Repeat {
-  id="prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
+  id="prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
   erls = Rule_Def.Repeat {
-    id="erls_prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
+    id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), 
     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [(*for precond NTH_CONS ...*)
   	   \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),