1.1 --- a/src/Tools/isac/Interpret/derive.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -14,11 +14,11 @@
     1.4    type step
     1.5    type derivation
     1.6  
     1.7 -  val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
     1.8 +  val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
     1.9      term option -> term -> derivation
    1.10 -  val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
    1.11 +  val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
    1.12      term option -> term -> rule_result list
    1.13 -  val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
    1.14 +  val steps : Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term ->
    1.15      bool * derivation
    1.16    val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
    1.17  \<^isac_test>\<open>