1.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 15:57:46 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 17:36:59 2022 +0200
     1.3 @@ -22,12 +22,12 @@
     1.4  
     1.5    val from_store: Tactic.input -> Error_Pattern_Def.id list
     1.6    val filled_exactly: Calc.T -> string -> string * Tactic.input
     1.7 -  val check_for: term * term -> term * Env.T -> T list * Rule_Set.T -> id option
     1.8 +  val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option
     1.9  
    1.10    val find_fill_patterns: Calc.T -> id -> record list
    1.11  
    1.12  \<^isac_test>\<open>
    1.13 -  val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
    1.14 +  val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option
    1.15    val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm ->
    1.16      record list
    1.17    val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
    1.18 @@ -54,9 +54,8 @@
    1.19  (*
    1.20    check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
    1.21  *)
    1.22 -fun check_for' (res, inf) subst (id, pat) rls =
    1.23 +fun check_for' ctxt (res, inf) subst (id, pat) rls =
    1.24    let
    1.25 -    val ctxt = Proof_Context.init_global ((ThyC.Isac()))
    1.26      val (res', _, _, rewritten) =
    1.27        Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
    1.28          Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.29 @@ -79,12 +78,12 @@
    1.30    check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
    1.31    (prog, env) for retrieval of casual substitution for bdv in the pattern.
    1.32  *)
    1.33 -fun check_for (res, inf) (prog, env) (errpats, rls) =
    1.34 +fun check_for ctxt (res, inf) (prog, env) (errpats, rls) =
    1.35    let
    1.36      val (_, subst) = Subst.for_bdv prog env
    1.37      fun scan (_, [], _) = NONE
    1.38        | scan (id, T :: errpats, _) =
    1.39 -          case check_for' (res, inf) subst (id, T) rls of
    1.40 +          case check_for' ctxt (res, inf) subst (id, T) rls of
    1.41              NONE => scan (id, errpats, [])
    1.42            | SOME id => SOME id
    1.43      fun scans [] = NONE