test/Tools/isac/Interpret/error-pattern.sml
changeset 60360 49680d595342
parent 60340 0ee698b0a703
child 60424 c3acf9c442ac
     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;