1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sat Oct 08 15:57:10 2022 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat Oct 08 19:17:24 2022 +0200
     1.3 @@ -1101,12 +1101,12 @@
     1.4      then () else error "find_fill_patterns changed 1a"
     1.5  | _ => error "find_fill_patterns changed 1b"
     1.6  
     1.7 -"~~~~~ fun fill_from_store, args:"; val (subst, form, errpatID, thm) =
     1.8 -  (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
     1.9 +"~~~~~ fun fill_from_store, args:"; val (ctxt, subst, form, errpatID, thm) =
    1.10 +  (ctxt, subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
    1.11          val thmDeriv = Thm.get_name_hint thm
    1.12          val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
    1.13          val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
    1.14 -        val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store theID
    1.15 +        val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store ctxt theID
    1.16          val some = map (Error_Pattern.fill_form ctxt subst (thm, form) errpatID) fillpats;
    1.17  
    1.18  case some |> filter is_some |> map the of