1.1 --- a/src/Tools/isac/Interpret/script.sml	Sun May 15 10:25:42 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Sun May 15 11:32:41 2011 +0200
     1.3 @@ -437,11 +437,13 @@
     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 +          |> declare_constraints' vals
    1.10  	      val hdl =
    1.11            case cas of
    1.12  		        NONE => pblterm dI pI
    1.13  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    1.14 -        val ctxt = declare_constraints' vals (ProofContext.init_global thy)
    1.15          val f = subpbl (strip_thy dI) pI
    1.16        in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    1.17        end
    1.18 @@ -618,16 +620,15 @@
    1.19  		        handle ERROR "actual args do not match formal args"
    1.20  			      => (match_ags_msg pI stac ags(*raise exn*);[]), mI);
    1.21          val (fmz_, vals) = oris2fmz_vals pors;
    1.22 -	      val {cas, ppc,...} = get_pbt pI
    1.23  	      val {cas, ppc, thy,...} = get_pbt pI
    1.24  	      val dI = theory2theory' thy (*take dI from _refined_ pbl*)
    1.25  	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
    1.26 -	      val thy' = (maxthy (assoc_thy dI) (rootthy pt))
    1.27 +	      val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
    1.28 +          |> declare_constraints' vals
    1.29  	      val hdl = 
    1.30            case cas of
    1.31  		        NONE => pblterm dI pI
    1.32  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    1.33 -        val ctxt = declare_constraints' vals (ProofContext.init_global thy')
    1.34          val f = subpbl (strip_thy dI) pI
    1.35        in 
    1.36          if domID = dI andalso pblID = pI