# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1659610117 -7200
# Node ID 2e0b7ca391dc4e7218e772400f7ea8ff3c850dd0
# Parent  ce09935439b309a90d4f18a6ade9a1464c76e879
polish naming in Rewrite_Order

diff -r ce09935439b3 -r 2e0b7ca391dc TODO.md
--- a/TODO.md	Wed Aug 03 18:17:27 2022 +0200
+++ b/TODO.md	Thu Aug 04 12:48:37 2022 +0200
@@ -50,7 +50,7 @@
     and all Isac_Knowledge is in session Isac.
     So Context.theory_name suffices
 
-* Eliminate mutable Rewrite_Ord.rew_ord' (!?);
+* Eliminate mutable Rewrite_Ord.id (!?);
     shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy
 
 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
diff -r ce09935439b3 -r 2e0b7ca391dc doc-isac/mat-eng-de.tex
--- a/doc-isac/mat-eng-de.tex	Wed Aug 03 18:17:27 2022 +0200
+++ b/doc-isac/mat-eng-de.tex	Thu Aug 04 12:48:37 2022 +0200
@@ -463,7 +463,7 @@
                   Thm
                      ("sym_rmult_assoc",
                         "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1"  [.])],
-               rew_ord = ("e_rew_ord", fn),
+               rew_ord = ("Rewrite_Ord.id_empty", fn),
                preconds = []} : rls
 \end{verbatim}}
 
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/Know_Store.thy
--- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -68,8 +68,8 @@
 *)
 signature KESTORE_ELEMS =
 sig
-  val get_rew_ord: theory -> Rewrite_Ord.rew_ord list
-  val add_rew_ord: Rewrite_Ord.rew_ord list -> theory -> theory
+  val get_rew_ord: theory -> Rewrite_Ord.T list
+  val add_rew_ord: Rewrite_Ord.T list -> theory -> theory
   val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
   val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
   val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/method-def.sml
--- a/src/Tools/isac/BaseDefinitions/method-def.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/method-def.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -37,7 +37,7 @@
   {guh       : Check_Unique.id,   (* unique within Isac_Knowledge, for html-presentation      *)
   mathauthors: string list,       (* copyright                                                *)
   init       : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly                *)
-  rew_ord'   : Rule_Def.rew_ord', (* for ordered rewriting by Tactic.Rewrite                  *)
+  rew_ord'   : Rewrite_Ord.id,    (* for ordered rewriting by Tactic.Rewrite                  *)
   erls       : Rule_Set.T,        (* for conditions in rewriting by Tactic.Rewrite            *)
   srls       : Rule_Set.T,        (* for evaluating Prog_Expr                                 *)
   crls       : Rule_Set.T,        (* DEL: for check_elementwise                               *)
@@ -50,7 +50,7 @@
                                      for constraints on identifiers see "O_Model.copy_name"   *)
   pre        : term list          (* ? DEL, as soon as they are input interactively ?         *)
 	};
-val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
+val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.id_empty,
 	erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
 	errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
 val empty_store = Store.Node ("empty_meth_id", [empty],[]);
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/rewrite-order.sml
--- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -4,16 +4,17 @@
 *)
 signature REWRITE_ORDER =
 sig
-  val e_rew_ord': Rule_Def.rew_ord';
-  val dummy_ord: Rule_Def.rew_ord_
-  val e_rew_ord: Rule_Def.rew_ord_
+  type id = Rule_Def.rew_ord_id
+  val id_empty: id
 
-  type rew_ord = Rule_Def.rew_ord
-  val e_rew_ordX: rew_ord
-  val to_string: rew_ord -> string
+  type function = Rule_Def.rew_ord_function
+  val function_empty: function
 
-  type rew_ord' = Rule_Def.rew_ord'
-  val equal: rew_ord * rew_ord -> bool
+  type T = Rule_Def.rew_ord_T
+  val empty: T
+
+  val to_string: T -> string
+  val equal: T * T -> bool
 end
 
 (**)
@@ -21,17 +22,16 @@
 struct
 (**)
 
-val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
-type rew_ord_ = Rule_Def.rew_ord_;
-fun dummy_ord (_: subst) (_: term, _: term) = true;
-val e_rew_ord_ = dummy_ord;
+type id = Rule_Def.rew_ord_id
+val id_empty = "Rewrite_Ord.id_empty";
 
-type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
-val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
-val e_rew_ordX = (e_rew_ord', e_rew_ord_)
+type function = Rule_Def.rew_ord_function;
+fun function_empty (_: LibraryC.subst) (_: term, _: term) = true;
+
+type T = Rule_Def.rew_ord_T
+val empty = (id_empty, function_empty)
+
 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
-
-type rew_ord' = Rule_Def.rew_ord'
 fun equal ((id1, _), (id2, _)) = id1 = id2
 
 end
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/rule-def.sml
--- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -10,19 +10,21 @@
   type calc
   eqtype calID
   eqtype errpatID
-  type rew_ord' = string
-  type rew_ord_ = LibraryC.subst -> term * term -> bool
-  type rew_ord = rew_ord' * rew_ord_
+
+  type rew_ord_id = string
+  type rew_ord_function = LibraryC.subst -> term * term -> bool
+  type rew_ord_T = rew_ord_id * rew_ord_function
+
   type eval_fn = string -> term -> Proof.context -> (string * term) option
 
   datatype rule_set =
        Empty
      | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
-       preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
+       preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
      | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
-       preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
+       preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
      | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
-       prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
+       prepat: (term list * term) list, rew_ord: rew_ord_T, scr: program}
   and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule
      | Rls_ of rule_set | Thm of string * thm
   and program =
@@ -44,9 +46,9 @@
 
 type eval_fn = string -> term -> Proof.context -> (string * term) option;
 
-type rew_ord' = string;
-type rew_ord_ = LibraryC.subst -> term * term -> bool;
-type rew_ord = rew_ord' * rew_ord_;
+type rew_ord_id = string;
+type rew_ord_function = LibraryC.subst -> term * term -> bool;
+type rew_ord_T = rew_ord_id * rew_ord_function;
 
 type calID = string;
 type cal = calID * eval_fn;
@@ -109,7 +111,7 @@
   | Repeat of         (*a confluent and terminating ruleset, in principle             *)
     {id: string,      (* for trace_rewrite                                            *)
      preconds: term list, (* STILL UNUSED                                             *)
-     rew_ord: rew_ord,(* for rules                                                    *)                                             
+     rew_ord: rew_ord_T,(* for rules                                                  *)                                             
      erls: rule_set,  (* for the conditions in rules                                  *)
      srls: rule_set,  (* for evaluation of Prog_Expr                                  *)
      calc: calc list, (* for Calculate in program, set by prep_rls'                   *)
@@ -117,7 +119,7 @@
      errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy              *)
      scr: program}    (* DEPRECATED: intersteps are created on the fly now            *)
   | Sequence of       (* a sequence of rules to be tried only once                    *)
-    {id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
+    {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set,
      calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
   | Rrls of           (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
     {id: string,      (* for trace_rewrite                                            *)
@@ -125,7 +127,7 @@
        (term list *   (* preconds, eval with subst from pattern below                 *)
 		     term)        (* pattern matched with current (sub)term                       *)
 		   list,          (* meta-conjunction in guarding is or                           *)
-     rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
+     rew_ord: rew_ord_T, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
 
 fun program_to_string Empty_Prog = "Empty_Prog"
   | program_to_string (Prog s) = "Prog " ^ UnparseC.term s
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/rule-set.sml
--- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -11,7 +11,7 @@
 
   val id: T -> string
   val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
-    preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
+    preconds: term list, rew_ord: Rewrite_Ord.T, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
   val to_string: T -> string
 
   val append_rules: string -> T -> Rule_Def.rule list -> T
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/thy-write.sml
--- a/src/Tools/isac/BaseDefinitions/thy-write.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/thy-write.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -12,7 +12,7 @@
   type authors
   datatype thydata
     = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
-    | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
+    | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rewrite_Ord.function}
     | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
     | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
     | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Interpret/derive.sml
--- a/src/Tools/isac/Interpret/derive.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Interpret/derive.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -14,11 +14,11 @@
   type step
   type derivation
 
-  val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
+  val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
     term option -> term -> derivation
-  val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
+  val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
     term option -> term -> rule_result list
-  val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
+  val steps : Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term ->
     bool * derivation
   val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
 \<^isac_test>\<open>
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Interpret/error-pattern.sml
--- a/src/Tools/isac/Interpret/error-pattern.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Interpret/error-pattern.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -58,7 +58,7 @@
   let
     val ctxt = Proof_Context.init_global ((ThyC.Isac()))
     val (res', _, _, rewritten) =
-      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord
+      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
         Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
   in
     if rewritten then 
@@ -100,7 +100,7 @@
   let
     val ctxt = Proof_Context.init_global ((ThyC.Isac()))
     val (form', _, _, rewritten) =
-      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
+      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
   in (*the fillpat of the thm must be dedicated to id*)
     if id = erpaID andalso rewritten then
       SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) 
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Interpret/solve-step.sml
--- a/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Interpret/solve-step.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -17,7 +17,7 @@
     theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
 
   val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
-    string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
+    string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
   val get_eval: string -> Pos.pos ->Ctree.ctree ->
     string * ThyC.id * (string * Rule_Def.eval_fn)
 \<^isac_test>\<open>
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Base_Tools.thy
--- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -50,15 +50,15 @@
   fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
 end;
 \<close> ML \<open>
-(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
-val tless_true = Rewrite_Ord.dummy_ord;
+(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*)
+val tless_true = Rewrite_Ord.function_empty;
 \<close> ML \<open>
 \<close> 
 setup \<open>KEStore_Elems.add_rew_ord [
   ("tless_true", tless_true),
-	("e_rew_ord", tless_true),
+	("Rewrite_Ord.id_empty", tless_true),
 	("e_rew_ord'", tless_true),
-	("dummy_ord", Rewrite_Ord.dummy_ord)]\<close>
+	("dummy_ord", Rewrite_Ord.function_empty)]\<close>
 
 subsection \<open>rule-sets\<close>
 ML \<open>
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -33,7 +33,7 @@
     (Try (Calculate ''TIMES''))) e_e)"
 
 method met_test_diophant : "Test/solve_diophant" =
-  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
+  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
     crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
   Program: diophant_equation.simps
   Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
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_"),
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -158,12 +158,12 @@
 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
 val norm_Rational_rls_noadd_fractions = 
   Rule_Def.Repeat {id = "norm_Rational_rls_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 = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
   	  Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
   		(Rule_Def.Repeat {id = "rat_mult_div_pow", 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-is_polyexp" Rule_Set.empty
   				 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
   			 srls = Rule_Set.Empty, calc = [], errpatts = [],
@@ -187,7 +187,7 @@
 (*.for simplify_Integral adapted from 'norm_Rational'.*)
 val norm_Rational_noadd_fractions = 
   Rule_Set.Sequence {id = "norm_Rational_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 = [Rule.Rls_ discard_minus,
   		Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)
@@ -214,7 +214,7 @@
 		];
 val simplify_Integral = 
   Rule_Set.Sequence {id = "simplify_Integral", 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 = [
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
--- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -27,7 +27,7 @@
 
 ML \<open>
 val inverse_z = prep_rls'(
-  Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
 	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 	  rules = 
 	   [
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -88,7 +88,7 @@
 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
 val LinEq_simplify = prep_rls'(
   Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
-    rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
+    rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
     erls = LinEq_erls,
     srls = Rule_Set.Empty,
     calc = [], errpatts = [],
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Partial_Fractions.thy
--- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -106,7 +106,7 @@
 
 ML \<open>
 val ansatz_rls = prep_rls'(
-  Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
 	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 	  rules = [
       \<^rule_thm>\<open>ansatz_2nd_order\<close>,
@@ -114,7 +114,7 @@
 	  scr = Rule.Empty_Prog});
 
 val equival_trans = prep_rls'(
-  Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
 	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 	  rules = [
       \<^rule_thm>\<open>equival_trans_2nd_order\<close>,
@@ -122,7 +122,7 @@
 	  scr = Rule.Empty_Prog});
 
 val multiply_ansatz = prep_rls'(
-  Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
 	  erls = Rule_Set.Empty,
 	  srls = Rule_Set.Empty, calc = [], errpatts = [],
 	  rules = [
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
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,
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 ""),
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,
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -439,7 +439,7 @@
 val rearrange_assoc =
   Rule_Def.Repeat{
     id = "rearrange_assoc", preconds = [], 
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), 
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), 
     erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm_sym>\<open>add.assoc\<close>,
@@ -461,7 +461,7 @@
 
 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
 val norm_equation =
-  Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+  Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>rnorm_equation_add\<close>],
@@ -525,7 +525,7 @@
 ML \<open>
 (*isolate the root in a root-equation*)
 val isolate_root =
-  Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), 
+  Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), 
     erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
     rules = [
        \<^rule_thm>\<open>rroot_to_lhs\<close>,
@@ -539,7 +539,7 @@
 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
 val isolate_bdv =
   Rule_Def.Repeat{
-    id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+    id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
   	erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
   	rules = [
       \<^rule_thm>\<open>risolate_bdv_add\<close>,
@@ -777,7 +777,7 @@
   in
     [e_e])"
 method met_test_solvelin : "Test/solve_linear" =
-  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
+  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
     prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
     nrls = Test_simplify}\<close>
   Program: solve_linear.simps
@@ -808,7 +808,7 @@
 
 method met_test_sqrt : "Test/sqrt-equ-test" =
   (*root-equation, version for tests before 8.01.01*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
         [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
     prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty 
@@ -834,7 +834,7 @@
 
 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
   (*tests subproblem fixed linear*)
-  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
+  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
      prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
        [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
      calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close>
@@ -864,7 +864,7 @@
 
 method met_test_eq1 : "Test/square_equation1" =
   (*root-equation1:*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
     prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
@@ -894,7 +894,7 @@
 
 method met_test_squ2 : "Test/square_equation2" =
   (*root-equation2*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
     prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
@@ -924,7 +924,7 @@
 
 method met_test_squeq : "Test/square_equation" =
   (*root-equation*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
     prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
@@ -947,7 +947,7 @@
 
 method met_test_eq_plain : "Test/solve_plain_square" =
   (*solve_plain_square*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
     prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
     asm_rls=[],asm_thm=[]*)}\<close>
   Program: solve_plain_square.simps
@@ -974,7 +974,7 @@
         [''no_met'']) [BOOL e_e, REAL v_v])"
 
 method met_test_norm_univ : "Test/norm_univar_equation" =
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
     errpats = [], nrls = Rule_Set.empty}\<close>
   Program: norm_univariate_equ.simps
   Given: "equality e_e" "solveFor v_v"
@@ -992,7 +992,7 @@
     (Try (Calculate ''TIMES''))) t_t)"
 
 method met_test_intsimp : "Test/intsimp" =
-  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,  prls = Rule_Set.empty, calc = [],
+  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,  prls = Rule_Set.empty, calc = [],
     crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
   Program: test_simplify.simps
   Given: "intTestGiven t_t"
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/MathEngBasic/method.sml
--- a/src/Tools/isac/MathEngBasic/method.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/MathEngBasic/method.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -42,7 +42,7 @@
 (* a subset of MethodC.T record's fields *)
 type input = 
   {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
-    prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
+    prls: Rule_Set.T, rew_ord': Rewrite_Ord.id, rls': Rule_Set.T, srls: Rule_Set.T}
 
 fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
 	    (metID, ppc,
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/MathEngBasic/rewrite.sml
--- a/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -10,19 +10,19 @@
   val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term
   val eval_true_: Proof.context -> Rule_Set.T -> term -> bool
   val eval_true: Proof.context -> term list -> Rule_Set.T -> bool
-  val rew_sub: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_
+  val rew_sub: Proof.context -> int -> Subst.T -> Rewrite_Ord.function
     -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
-  val rewrite_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
+  val rewrite_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm ->
     term -> (term * term list) option
-  val rewrite_inst_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
+  val rewrite_inst_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool
     -> Subst.T -> thm -> term -> (term * term list) option
   val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option
   val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
-  val rewrite_terms_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
+  val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list
     -> term -> (term * term list) option
 
 \<^isac_test>\<open>
-  val rewrite__: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ ->
+  val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function ->
     Rule_Set.T -> bool -> thm -> term -> (term * term list) option
   val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
   val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
@@ -287,7 +287,7 @@
   case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of
 	  NONE => NONE
 	| SOME (thmID, thm) =>
-	  (let val rew = case rewrite_ ctxt Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of
+	  (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of
         SOME (rew, _) => rew
       | NONE => raise ERROR (msg "calculate_" ctxt id thm t)
     in SOME (rew, (thmID, thm)) end)
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/MathEngBasic/state-steps.sml
--- a/src/Tools/isac/MathEngBasic/state-steps.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -12,7 +12,7 @@
   type T
   val to_string : T -> string
   val result : single -> (term * term list)
-  val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
+  val make_single: Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
     single
   val insert_pos : Pos.pos -> T -> T
 end
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/MathEngBasic/tactic.sml
--- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/MathEngBasic/tactic.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -28,12 +28,12 @@
   | Empty_Tac_
   | Free_Solve'
   | Or_to_List' of term * term
-  | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
-  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
+  | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
+  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
   | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
   | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
   | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term
-  | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
+  | Substitute' of Rewrite_Ord.function * Rule_Set.T * Subst.as_eqs * term * term
 (*RM*)| Tac_ of theory * string * string * string
   | Take' of term
   | End_Detail' of Celem.result
@@ -240,7 +240,7 @@
 
 (* try if a rewrite-rule is applicable to a given formula; 
    in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 
-fun try_rew ctxt ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
+fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
     if Auto_Prog.contains_bdv thm
     then case Rewrite.rewrite_inst_ ctxt ro erls false subst thm f of
 	    SOME _ => [rule2tac ctxt subst thm']
@@ -268,7 +268,7 @@
 (* decide if a tactic is applicable to a given formula; 
    in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
 fun applicable ctxt _ _ f (Calculate scrID) =
-    try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f 
+    try_rew ctxt Rewrite_Ord.empty Rule_Set.empty [] f 
       (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
   | applicable ctxt ro erls f (Rewrite thm'') =
     try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')
@@ -325,8 +325,8 @@
   | Empty_Tac_
   | Free_Solve'
   | Or_to_List' of term * term
-  | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
-  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
+  | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
+  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
   | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
   | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
   | Subproblem' of       (* switch from solve-phase to specify-phase         *)
@@ -337,7 +337,7 @@
       Proof.context *    (* for the specify-phase                            *)
   		term               (* Subproblem (thyID, pbl) OR CAS_Cmd               *)  
   | Substitute' of       (* substitute variables (TODO: from the context)    *)    
-      Rule_Def.rew_ord_ *(* for re-calculation                               *)
+      Rewrite_Ord.function *(* for re-calculation                               *)
       Rule_Set.T *       (* for re-calculation                               *)
       Subst.as_eqs *     (* the substitution: terms of type bool             *)
       term *             (* to be substituted into                           *)
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -131,7 +131,7 @@
 ML \<open>
 \<close> ML \<open>
 val prog_expr =
-  Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
     rules = [Rule_Def.Thm ("refl",  @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
        Rule_Def.Thm ("o_apply",  @{thm o_apply}),
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/ProgLang/Prog_Expr.thy
--- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -263,13 +263,13 @@
 > reflI;
 val it = "(?t = ?t) = True"
 > val t = str2term "x = 0";
-> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
+> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
 
 > val t = str2term "1 = 0";
-> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
+> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
 ----------- thus needs Rule.Eval !
 > val t = str2term "0 = 0";
-> val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
+> val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
 > UnparseC.term t';
 val it = \<^const_name>\<open>True\<close>
 
diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/TODO.thy
--- a/src/Tools/isac/TODO.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/TODO.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -274,7 +274,7 @@
   \item Diff.thy: differentiateX --> differentiate after removal of script-constant
   \item Test.thy: met_test_sqrt2: deleted?!
   \item xxx          
-  \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx, too*)
+  \item Rewrite_Ord.id := overwritel (! Rewrite_Ord.id, (*<<<---- use Know_Store.xxx, too*)
   \item xxx
     \item automatically extrac rls from program-code 
       ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Interpret/error-pattern.sml
--- a/test/Tools/isac/Interpret/error-pattern.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Interpret/error-pattern.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -909,7 +909,7 @@
 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2");
 
 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
-  rew_sub ctxt 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
+  rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
 if rewritten then NONE else SOME "e_errpatID";
 
 val norm_res = case rewrite_set_ ctxt false rls res' of
@@ -957,7 +957,7 @@
 val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)");
 
 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
-  rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
+  rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
 if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
 else error "build fun check_for' ?bdv changed 2";
 
@@ -1119,7 +1119,7 @@
   val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
   (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
 val (form', _, _, rewritten) =
-      rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
+      rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
 
 if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then ()
 else error "find_fill_patterns changed 3";
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/algein.sml
--- a/test/Tools/isac/Knowledge/algein.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/algein.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -99,7 +99,7 @@
 "----------- Widerspruch 3 = 777 ---------------------------------";
 val thy = @{theory "Isac_Knowledge"}; 
 val ctxt = Proof_Context.init_global thy;
-val rew_ord = dummy_ord;
+val rew_ord = Rewrite_Ord.function_empty;
 val erls = Rule_Set.Empty;
 val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
 val t = TermC.str2term "0 = (0::real)";
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/diophanteq.sml
--- a/test/Tools/isac/Knowledge/diophanteq.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -33,7 +33,7 @@
       SOME t' => t'
     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
 
-val SOME (t,_) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst 
+val SOME (t,_) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst 
   @{thm "int_isolate_add"} t; UnparseC.term t;
 
 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/eqsystem-1.sml
--- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -221,7 +221,7 @@
 val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
 	    (TermC.str2term"bdv_2",TermC.str2term"c_2")];
-val SOME (e2__,_) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty [e1__] e2__;
+val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
 else error "eqsystem.sml top_down_substitution,2x2] subst";
 
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/eqsystem-2.sml
--- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -207,9 +207,9 @@
   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
   "0 = c_4, " ^
   "0 = c_3]");
-val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
-val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
-val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
+val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
+val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
+val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
 if UnparseC.term t = 
   "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/poly-1.sml
--- a/test/Tools/isac/Knowledge/poly-1.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/poly-1.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -470,7 +470,7 @@
 
 "----- eval_is_multUnordered ---";
 val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +  (-48 * x \<up> 4 + 8))) is_multUnordered";
-case eval_is_multUnordered "testid" "" tm thy of
+case eval_is_multUnordered "testid" "" tm @{context} of
     SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
                    (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
                           (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 
@@ -492,7 +492,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables  3 * a + - 2 * a   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx 3 * a + - 2 * a_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -507,7 +507,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables  - 2 * a   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx - 2 * a_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -521,7 +521,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables   a   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx a_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -535,7 +535,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables   - 2   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx - 2_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -676,7 +676,7 @@
 val t = TermC.str2term "(6 * a) is_multUnordered"; 
 val SOME
     (_, t') =
-           eval_is_multUnordered "xxx" () t @{theory};
+           eval_is_multUnordered "xxx" () t @{context};
 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () 
 (*+*)else error "6 * a is_multUnordered = False CHANGED";
 
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/polyeq-1.sml
--- a/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -1018,31 +1018,31 @@
 then () else error "rls complete_square CHANGED";
 
 val thm = @{thm square_explicit1};
-val SOME (t,asm) = rewrite_ ctxt dummy_ord Rule_Set.Empty true thm t;
+val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true thm t;
 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
 then () else error "thm square_explicit1 CHANGED";
 
 val thm = @{thm root_plus_minus};
-val SOME (t,asm) = rewrite_ ctxt dummy_ord PolyEq_erls true thm t;
+val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty PolyEq_erls true thm t;
 if UnparseC.term t =
 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
 then () else error "thm root_plus_minus CHANGED";
 
 (*the thm bdv_explicit2* here required to be constrained to ::real*)
 val thm = @{thm bdv_explicit2};
-val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
+val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
 if UnparseC.term t =
 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
 then () else error "thm bdv_explicit2 CHANGED";
 
 val thm = @{thm bdv_explicit3};
-val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
+val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
 if UnparseC.term t =
 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
 then () else error "thm bdv_explicit3 CHANGED";
 
 val thm = @{thm bdv_explicit2};
-val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
+val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
 if UnparseC.term t =
 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
 then () else error "thm bdv_explicit2 CHANGED";
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/polyeq-2.sml
--- a/test/Tools/isac/Knowledge/polyeq-2.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -287,14 +287,14 @@
 t |> UnparseC.term; t |> TermC.atomty;
 val thm = @{thm d2_prescind1};
 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
-val SOME (t', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
+val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t';
 
 (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) 
                                                                         --> x = 0 | -6 + 5 * x = 0*)
 t' |> UnparseC.term; t' |> TermC.atomty;
 val thm = @{thm d2_reduce_equation1};
 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
-val SOME (t'', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
+val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t'';
 (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
 *)
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -257,7 +257,7 @@
   | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
 
 "======= compare tausche_plus with real_num_collect";
-val od = dummy_ord;
+val od = Rewrite_Ord.function_empty;
 
 val erls = erls_ordne_alphabetisch;
 val t = TermC.str2term "b + a";
@@ -526,12 +526,12 @@
 val erls = erls_ordne_alphabetisch;
 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 val SOME (t',_) = 
-    rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus} t;
+    rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus} t;
 UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
 
 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 val NONE = 
-    rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus_plus} t;
+    rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus_plus} t;
 
 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 val SOME (t',_) = 
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/rational-2.sml
--- a/test/Tools/isac/Knowledge/rational-2.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/rational-2.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -854,7 +854,7 @@
 "HOL.True";
 
 val t = TermC.str2term "(6*x) \<up> 2";
-val SOME (t',_) = rewrite_ ctxt dummy_ord powers_erls false @{thm realpow_def_atom} t;
+val SOME (t',_) = rewrite_ ctxt Rewrite_Ord.function_empty powers_erls false @{thm realpow_def_atom} t;
 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()
 else error "rational.sml powers_erls (6*x) \<up> 2";
 
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/MathEngBasic/rewrite.sml
--- a/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -88,7 +88,7 @@
 val thm =  @{thm add.commute};
 val tm = @{term "x + y*z::real"};
 
-val SOME (r,_) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
+val SOME (r,_) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
 (*is displayed on _TOP_ of <response> buffer...*)
 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
 if r = @{term "y*z + x::real"}
@@ -97,7 +97,7 @@
 "----- rewriting a subterm";
 val tm = @{term "w*(x + y*z)::real"};
 
-val SOME (r, _) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
+val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
 
 "----- ordered rewriting";
 fun tord (_:subst) pp = LibraryC.termless pp;
@@ -150,7 +150,7 @@
 val thm =  @{thm nonzero_divide_mult_cancel_right};
 val tm = @{term "x / (2 * x)::real"};
 
-val SOME (rew, asm) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
+val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
 
 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
 else error "rewrite.sml diff.result in cond.rew.";
@@ -168,12 +168,12 @@
 val tm = @{term "x / (2 * x)::real"};
 val erls = eval_rls;
 
-(**)val SOME (rew, asm) = rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm;
+(**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
   dest_Trueprop
   ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
-  (thy, dummy_ord, erls, false, thm, tm);
+  (thy, Rewrite_Ord.function_empty, erls, false, thm, tm);
 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
   (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
 
@@ -210,11 +210,11 @@
 "----------- step through 'and rew_sub': ----------------";
 (*and make asms without Trueprop, beginning with the result:*)
 val tm = @{term "x / (2 * x)::real"};
-val (t', asm, _, _) = rew_sub ctxt 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
+val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true [] (Thm.prop_of thm) tm;
 (*show_types := false;*)
 "----- evaluate arguments";
 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
-    (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
+    (thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
 "----- step 1: LHS, RHS of rule";
      val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
                        o Logic.strip_imp_concl) r;
@@ -245,7 +245,7 @@
 "----------- step through 'fun rewrite_terms_'  ------------------------------------------------";
 "----- step 0: args for rewrite_terms_, local fun";
 val (thy, ord, erls, equs, t) =
-    (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
+    (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"],
      TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
 "----- step 1: args for rew_";
 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
@@ -254,21 +254,21 @@
 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
 
 
-val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
+val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
 writeln "---------- rewrite_terms_  1---------------------------";
 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [x = 0]";
 
 val equs = [TermC.str2term "M_b 0 = 0"];
 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
-val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
+val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
 writeln "---------- rewrite_terms_  2---------------------------";
 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
 
 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
-val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
+val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
 writeln "---------- rewrite_terms_  3---------------------------";
 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
@@ -658,7 +658,7 @@
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
-  (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
+  (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
   (thy, 1, [], rew_ord, erls, bool, thm, term);
 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/MathEngBasic/tactic.sml
--- a/test/Tools/isac/MathEngBasic/tactic.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/MathEngBasic/tactic.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -18,7 +18,7 @@
 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
 ;
-Rewrite': ThyC.id * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
+Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
 ;
 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/ProgLang/calculate.sml
--- a/test/Tools/isac/ProgLang/calculate.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/ProgLang/calculate.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -15,7 +15,8 @@
 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
 
-fun test thy t = writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul thy t)));
+fun test thy t = 
+  writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul @{context} t)));
 
 test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
 test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/ProgLang/evaluate.sml
--- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/ProgLang/evaluate.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -56,22 +56,22 @@
 
 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
-val SOME (t', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_  1 + 2 = 3  changed";
 
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
-val SOME (t'', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_  3 * 4 = 12  changed";
 
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
-val SOME (t''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_  12 / 3 = 4  changed";
 
 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
-val SOME (t'''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
+val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
 if UnparseC.term t'''' = "16" then () else error "calculate_  12 / 3 = 4  changed";
 
 "----------- calculate from Prog --------------------------------- -----------------------------";
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/ProgLang/listC.sml
--- a/test/Tools/isac/ProgLang/listC.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/ProgLang/listC.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -51,7 +51,7 @@
 TermC.atomty t;
 val thm = Thm.prop_of @{thm NTH_NIL};
 TermC.atomty thm;
-val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_NIL} t;
+val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;
 if UnparseC.term t' = "a" then () 
 else error "NTH 1 [a,b,c,d,e] = a ..changed";
 
@@ -66,7 +66,7 @@
 | _ => error "ListC.NTH changed";
 val thm = Thm.prop_of @{thm NTH_CONS};
 TermC.atomty thm;
-val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false  @{thm NTH_CONS} t;
+val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false  @{thm NTH_CONS} t;
 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
 
diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Test_Isac_Short.thy
--- a/test/Tools/isac/Test_Isac_Short.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Test_Isac_Short.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -145,19 +145,12 @@
 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
 \<close> ML \<open>
 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
-Rewrite.trace_on := false;
 \<close>
 ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
 \<close>
 
 ML \<open>
@@ -333,12 +326,6 @@
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
 \<close>
 
 section \<open>history of tests\<close>