src/Tools/isac/Interpret/solve.sml
branchdecompose-isar
changeset 42023 927cb6806af1
parent 42018 11cf93cd02c6
child 42090 908dfde7cf75
     1.1 --- a/src/Tools/isac/Interpret/solve.sml	Sat May 21 09:54:39 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Sat May 21 12:52:59 2011 +0200
     1.3 @@ -212,7 +212,7 @@
     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 ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
     1.9              val ((p,p_),ps,f,pt) = 
    1.10  	            generate1 thy (Check_Postcond' (pI, (scval, asm)))
    1.11  		            (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
    1.12 @@ -332,7 +332,7 @@
    1.13  	          val metID = get_obj g_metID pt ppp;
    1.14  	          val {scr,...} = get_met metID;
    1.15              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
    1.16 -	          val ctxt'' = transfer_from_subproblem ctxt ctxt'
    1.17 +	          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
    1.18              val tac_ = Check_Postcond' (pI, (scval, asm))
    1.19  	          val is = ScrState (E,l,a,scval,scsaf,b)
    1.20              val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;