diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Interpret/error-pattern.sml
--- a/src/Tools/isac/Interpret/error-pattern.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Interpret/error-pattern.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -58,7 +58,7 @@
   let
     val ctxt = Proof_Context.init_global ((ThyC.Isac()))
     val (res', _, _, rewritten) =
-      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord
+      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
         Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
   in
     if rewritten then 
@@ -100,7 +100,7 @@
   let
     val ctxt = Proof_Context.init_global ((ThyC.Isac()))
     val (form', _, _, rewritten) =
-      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
+      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
   in (*the fillpat of the thm must be dedicated to id*)
     if id = erpaID andalso rewritten then
       SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)