1.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4    let
     1.5      val ctxt = Proof_Context.init_global ((ThyC.Isac()))
     1.6      val (res', _, _, rewritten) =
     1.7 -      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord
     1.8 +      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
     1.9          Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.10    in
    1.11      if rewritten then 
    1.12 @@ -100,7 +100,7 @@
    1.13    let
    1.14      val ctxt = Proof_Context.init_global ((ThyC.Isac()))
    1.15      val (form', _, _, rewritten) =
    1.16 -      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.17 +      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.18    in (*the fillpat of the thm must be dedicated to id*)
    1.19      if id = erpaID andalso rewritten then
    1.20        SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)