diff -r 5e1e45b3ddef -r 4162c4f6f897 src/Tools/isac/Interpret/script.sml
--- a/src/Tools/isac/Interpret/script.sml	Fri Oct 12 16:03:07 2012 +0200
+++ b/src/Tools/isac/Interpret/script.sml	Fri Oct 12 17:06:58 2012 +0200
@@ -429,8 +429,8 @@
 	      val {cas,ppc,thy,...} = get_pbt pI
 	      val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
 	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
-        val ctxt = ProofContext.init_global 
-        val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
+        val ctxt = Proof_Context.init_global 
+        val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 
           |> declare_constraints' vals
 	      val hdl =
           case cas of
@@ -626,7 +626,7 @@
 	      val {cas, ppc, thy,...} = get_pbt pI
 	      val dI = theory2theory' thy (*take dI from _refined_ pbl*)
 	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
-	      val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
+	      val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 
           |> declare_constraints' vals
 	      val hdl = 
           case cas of
@@ -1557,7 +1557,7 @@
 			      "formals: " ^ terms2str formals ^ "\n" ^
 			      "actuals: " ^ terms2str actuals)
      val env = relate_args [] formals actuals;
-     val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
+     val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
      val {pre, prls, ...} = get_met metID;
      val pres = check_preconds thy prls pre itms |> map snd;
      val ctxt = ctxt |> insert_assumptions pres;