1.1 --- a/src/Tools/isac/Interpret/appl.sml	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -345,7 +345,7 @@
     1.4            val pres = map (mk_env probl |> subst_atomic) where_
     1.5            val ctxt = 
     1.6              if is_e_ctxt ctxt
     1.7 -            then assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres
     1.8 +            then assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres
     1.9              else ctxt
    1.10           (*TODO.WN110416 here do evalprecond according to fun check_preconds'
    1.11           and then decide on Notappl/Appl accordingly once more.