1.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -55,16 +55,18 @@
     1.4    check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
     1.5  *)
     1.6  fun check_for' (res, inf) subst (id, pat) rls =
     1.7 -  let 
     1.8 -    val (res', _, _, rewritten) = Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord
     1.9 -      Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.10 +  let
    1.11 +    val ctxt = Proof_Context.init_global ((ThyC.Isac()))
    1.12 +    val (res', _, _, rewritten) =
    1.13 +      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord
    1.14 +        Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.15    in
    1.16      if rewritten then 
    1.17        let
    1.18 -        val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls  res' of
    1.19 +        val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls  res' of
    1.20              NONE => res'
    1.21            | SOME (norm_res, _) => norm_res
    1.22 -        val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
    1.23 +        val norm_inf = case Rewrite.rewrite_set_inst_ ctxt false subst rls inf of
    1.24              NONE => inf
    1.25            | SOME (norm_inf, _) => norm_inf
    1.26        in
    1.27 @@ -96,8 +98,9 @@
    1.28    returns thm required by "fun in_fillform *)
    1.29  fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =
    1.30    let
    1.31 +    val ctxt = Proof_Context.init_global ((ThyC.Isac()))
    1.32      val (form', _, _, rewritten) =
    1.33 -      Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.34 +      Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.35    in (*the fillpat of the thm must be dedicated to id*)
    1.36      if id = erpaID andalso rewritten then
    1.37        SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)