1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -429,8 +429,8 @@
     1.4  	      val {cas,ppc,thy,...} = get_pbt pI
     1.5  	      val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
     1.6  	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
     1.7 -        val ctxt = ProofContext.init_global 
     1.8 -        val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
     1.9 +        val ctxt = Proof_Context.init_global 
    1.10 +        val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 
    1.11            |> declare_constraints' vals
    1.12  	      val hdl =
    1.13            case cas of
    1.14 @@ -626,7 +626,7 @@
    1.15  	      val {cas, ppc, thy,...} = get_pbt pI
    1.16  	      val dI = theory2theory' thy (*take dI from _refined_ pbl*)
    1.17  	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
    1.18 -	      val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
    1.19 +	      val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 
    1.20            |> declare_constraints' vals
    1.21  	      val hdl = 
    1.22            case cas of
    1.23 @@ -1557,7 +1557,7 @@
    1.24  			      "formals: " ^ terms2str formals ^ "\n" ^
    1.25  			      "actuals: " ^ terms2str actuals)
    1.26       val env = relate_args [] formals actuals;
    1.27 -     val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
    1.28 +     val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
    1.29       val {pre, prls, ...} = get_met metID;
    1.30       val pres = check_preconds thy prls pre itms |> map snd;
    1.31       val ctxt = ctxt |> insert_assumptions pres;