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                           *)