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>