1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 13 14:15:59 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 13 17:19:38 2011 +0200
     1.3 @@ -410,10 +410,10 @@
     1.4    | stac2tac_ pt thy (Const ("Script.Tac",_) $ Free (str,_)) = 
     1.5        (Tac ((de_esc_underscore o strip_thy) str),  Empty_Tac_) 
     1.6  
     1.7 +    (*compare "| assod _ (Subproblem'"*)
     1.8    | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
     1.9  	  (Const ("Product_Type.Pair",_) $Free (dI',_) $ 
    1.10  		 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
    1.11 -      (*compare "| assod _ (Subproblem'"*)
    1.12        let
    1.13          val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
    1.14          val thy = maxthy (assoc_thy dI) (rootthy pt);
    1.15 @@ -441,8 +441,9 @@
    1.16            case cas of
    1.17  		        NONE => pblterm dI pI
    1.18  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    1.19 +        val ctxt = declare_constraints' vals (ProofContext.init_global thy)
    1.20          val f = subpbl (strip_thy dI) pI
    1.21 -      in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f))
    1.22 +      in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    1.23        end
    1.24  
    1.25    | stac2tac_ pt thy t = error 
    1.26 @@ -592,10 +593,10 @@
    1.27        then Ass (m, ((term_of o the o (parse thy)) f'))
    1.28        else NotAss
    1.29  
    1.30 +    (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
    1.31    | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f))
    1.32  	  (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
    1.33  		 Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
    1.34 -      (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
    1.35        let 
    1.36          val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
    1.37          val thy = maxthy (assoc_thy dI) (rootthy pt);
    1.38 @@ -621,14 +622,16 @@
    1.39  	      val {cas, ppc, thy,...} = get_pbt pI
    1.40  	      val dI = theory2theory' thy (*take dI from _refined_ pbl*)
    1.41  	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
    1.42 +	      val thy' = (maxthy (assoc_thy dI) (rootthy pt))
    1.43  	      val hdl = 
    1.44            case cas of
    1.45  		        NONE => pblterm dI pI
    1.46  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    1.47 +        val ctxt = declare_constraints' vals (ProofContext.init_global thy')
    1.48          val f = subpbl (strip_thy dI) pI
    1.49        in 
    1.50          if domID = dI andalso pblID = pI
    1.51 -        then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f), f) 
    1.52 +        then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f) 
    1.53          else NotAss
    1.54        end
    1.55