1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -10,19 +10,19 @@
     1.4    val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term
     1.5    val eval_true_: Proof.context -> Rule_Set.T -> term -> bool
     1.6    val eval_true: Proof.context -> term list -> Rule_Set.T -> bool
     1.7 -  val rew_sub: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_
     1.8 +  val rew_sub: Proof.context -> int -> Subst.T -> Rewrite_Ord.function
     1.9      -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
    1.10 -  val rewrite_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
    1.11 +  val rewrite_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm ->
    1.12      term -> (term * term list) option
    1.13 -  val rewrite_inst_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
    1.14 +  val rewrite_inst_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool
    1.15      -> Subst.T -> thm -> term -> (term * term list) option
    1.16    val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option
    1.17    val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
    1.18 -  val rewrite_terms_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
    1.19 +  val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list
    1.20      -> term -> (term * term list) option
    1.21  
    1.22  \<^isac_test>\<open>
    1.23 -  val rewrite__: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ ->
    1.24 +  val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function ->
    1.25      Rule_Set.T -> bool -> thm -> term -> (term * term list) option
    1.26    val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
    1.27    val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
    1.28 @@ -287,7 +287,7 @@
    1.29    case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of
    1.30  	  NONE => NONE
    1.31  	| SOME (thmID, thm) =>
    1.32 -	  (let val rew = case rewrite_ ctxt Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of
    1.33 +	  (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of
    1.34          SOME (rew, _) => rew
    1.35        | NONE => raise ERROR (msg "calculate_" ctxt id thm t)
    1.36      in SOME (rew, (thmID, thm)) end)