1.1 --- a/src/Tools/isac/Interpret/solve.sml	Mon Apr 18 14:43:26 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Apr 18 15:24:57 2011 +0200
     1.3 @@ -227,12 +227,13 @@
     1.4  	val metID = get_obj g_metID pt ppp;
     1.5          val sc = (#scr o get_met) metID;
     1.6          val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); 
     1.7 +	      val ctxt'' = transfer_from_subproblem ctxt ctxt'
     1.8          val ((p,p_),ps,f,pt) = 
     1.9  	    generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
    1.10  		(ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
    1.11         in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
    1.12  	   ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
    1.13 -	      ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_))))
    1.14 +	      ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
    1.15  	end
    1.16      end
    1.17  (* val (msg, cs') = 
    1.18 @@ -373,12 +374,13 @@
    1.19          val thy = assoc_thy thy';
    1.20  	val metID = get_obj g_metID pt ppp;
    1.21  	val {scr,...} = get_met metID;
    1.22 -        val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm)
    1.23 +        val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
    1.24 +	      val ctxt'' = transfer_from_subproblem ctxt ctxt'
    1.25          val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
    1.26  	val is = ScrState (E,l,a,scval,scsaf,b)
    1.27 -        val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt;
    1.28 +        val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
    1.29  	(*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
    1.30 -       in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end
    1.31 +       in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
    1.32      end
    1.33  
    1.34    | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)