1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -73,8 +73,8 @@
     1.4  val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
     1.5  val ctxt = get_obj g_ctxt pt [];
     1.6  if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
     1.7 -val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});
     1.8 -if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name) = "Isac"
     1.9 +val pt = update_ctxt pt [] (Proof_Context.init_global @{theory "Isac"});
    1.10 +if (get_obj g_ctxt pt [] |> Proof_Context.theory_of |> Context.theory_name) = "Isac"
    1.11  then () else error "--- fun update_ctxt, fun g_ctxt changed";
    1.12  
    1.13  "-------------- check positions in miniscript --------------------";