1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Aug 10 10:27:15 2021 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Aug 10 11:01:18 2021 +0200
1.3 @@ -1216,7 +1216,7 @@
1.4 val pos = get_pos cI 1;
1.5
1.6 "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
1.7 - val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr
1.8 + val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr
1.9 val p' = lev_on p;
1.10 val tac = get_obj g_tac pt p';
1.11 val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;