diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -409,7 +409,7 @@
 (* evaluates conditions in calculate_Rational *)
 val calc_rat_erls =
   prep_rls'
-    (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+    (Rule_Def.Repeat {id = "calc_rat_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_"),
@@ -424,7 +424,7 @@
    need to have constants to be commuted together respectively           *)
 val calculate_Rational =
   prep_rls' (Rule_Set.merge "calculate_Rational"
-    (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+    (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
       erls = calc_rat_erls, srls = Rule_Set.Empty,
       calc = [], errpatts = [],
       rules = [
@@ -606,7 +606,7 @@
 (*.all powers over + distributed; atoms over * collected, other distributed
    contains absolute minimum of thms for context in norm_Rational .*)
 val powers = prep_rls'(
-  Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
       erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [
         \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s)  \<up>  n = r  \<up>  n * s  \<up>  n"*)
@@ -630,7 +630,7 @@
 (*.contains absolute minimum of thms for context in norm_Rational.*)
 val rat_mult_divide = prep_rls'(
   Rule_Def.Repeat {id = "rat_mult_divide", 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>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
@@ -647,7 +647,7 @@
 \<close> ML \<open>
 (*.contains absolute minimum of thms for context in norm_Rational.*)
 val reduce_0_1_2 = prep_rls'(
-  Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+  Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
@@ -670,7 +670,7 @@
 (*erls for calculate_Rational; 
   make local with FIXX@ME result:term *term list WN0609???SKMG*)
 val norm_rat_erls = prep_rls'(
-  Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
@@ -683,7 +683,7 @@
   which is now replaced by MGs version "norm_Rational" below
 *)
 val norm_Rational_min = prep_rls'(
-  Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], 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,
@@ -701,7 +701,7 @@
 \<close> ML \<open>
 val norm_Rational_parenthesized = prep_rls'(
   Rule_Set.Sequence {id = "norm_Rational_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 = [
@@ -723,7 +723,7 @@
       \<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]);
 
 val add_fractions_p_rls = prep_rls'(
-  Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
 	  erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 	  rules = [Rule.Rls_ add_fractions_p], 
 	  scr = Rule.Empty_Prog});
@@ -731,7 +731,7 @@
 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
 val cancel_p_rls = prep_rls'(
   Rule_Def.Repeat 
-    {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+    {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [Rule.Rls_ cancel_p], 
 	  scr = Rule.Empty_Prog});
@@ -739,7 +739,7 @@
 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
     used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
 val rat_mult_poly = prep_rls'(
-  Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
 	  erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [
      \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
 	  srls = Rule_Set.Empty, calc = [], errpatts = [],
@@ -754,7 +754,7 @@
     I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028 
     ... WN0609???MG.*)
 val rat_mult_div_pow = prep_rls'(
-  Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
@@ -770,7 +770,7 @@
     scr = Rule.Empty_Prog});
 
 val rat_reduce_1 = prep_rls'(
-  Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], 
     rules = [
       \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
@@ -779,7 +779,7 @@
 
 (* looping part of norm_Rational *)
 val norm_Rational_rls = prep_rls' (
-  Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       Rule.Rls_ add_fractions_p_rls,
@@ -791,7 +791,7 @@
 
 val norm_Rational = prep_rls' (
   Rule_Set.Sequence 
-    {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+    {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       Rule.Rls_ discard_minus,