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)