1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Mon Apr 18 14:43:26 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Mon Apr 18 15:24:57 2011 +0200
     1.3 @@ -1887,6 +1887,7 @@
     1.4  fun pt_extract (pt,([],Res)) =
     1.5  (* val (pt,([],Res)) = ptp;
     1.6     *)
     1.7 +    (* ML_TODO 110417 get assumptions from ctxt !? *)
     1.8      let val (f, asm) = get_obj g_result pt []
     1.9      in (Form f, NONE, asm) end
    1.10  (* val p = [3,2];

     2.1 --- a/src/Tools/isac/Interpret/mstools.sml	Mon Apr 18 14:43:26 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Mon Apr 18 15:24:57 2011 +0200
     2.3 @@ -158,6 +158,8 @@
     2.4      val insert_assumptions : term list -> Proof.context -> Proof.context
     2.5      val insert_environments :
     2.6            (term * term) list -> Proof.context -> Proof.context
     2.7 +    val transfer_from_subproblem :
     2.8 +          Proof.context -> Proof.context -> Proof.context
     2.9  
    2.10    end
    2.11  
    2.12 @@ -1006,6 +1008,9 @@
    2.13    fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt;
    2.14  end
    2.15  
    2.16 +fun transfer_from_subproblem ctxt_sub ctxt =
    2.17 +  insert_assumptions (get_assumptions ctxt_sub) ctxt;
    2.18 +
    2.19  (*----------------------------------------------------------*)
    2.20  end
    2.21  open SpecifyTools;

     3.1 --- a/src/Tools/isac/Interpret/solve.sml	Mon Apr 18 14:43:26 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Apr 18 15:24:57 2011 +0200
     3.3 @@ -227,12 +227,13 @@
     3.4  	val metID = get_obj g_metID pt ppp;
     3.5          val sc = (#scr o get_met) metID;
     3.6          val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); 
     3.7 +	      val ctxt'' = transfer_from_subproblem ctxt ctxt'
     3.8          val ((p,p_),ps,f,pt) = 
     3.9  	    generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
    3.10  		(ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
    3.11         in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
    3.12  	   ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
    3.13 -	      ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_))))
    3.14 +	      ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
    3.15  	end
    3.16      end
    3.17  (* val (msg, cs') = 
    3.18 @@ -373,12 +374,13 @@
    3.19          val thy = assoc_thy thy';
    3.20  	val metID = get_obj g_metID pt ppp;
    3.21  	val {scr,...} = get_met metID;
    3.22 -        val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm)
    3.23 +        val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
    3.24 +	      val ctxt'' = transfer_from_subproblem ctxt ctxt'
    3.25          val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
    3.26  	val is = ScrState (E,l,a,scval,scsaf,b)
    3.27 -        val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt;
    3.28 +        val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
    3.29  	(*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
    3.30 -       in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end
    3.31 +       in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
    3.32      end
    3.33  
    3.34    | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)

     4.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Apr 18 14:43:26 2011 +0200
     4.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Apr 18 15:24:57 2011 +0200
     4.3 @@ -93,19 +93,6 @@
     4.4  (*use "Interpret/solve.sml"           TODO*)
     4.5  (*use "Interpret/inform.sml"          TODO*)
     4.6    use "Interpret/mathengine.sml"(*part.*)
     4.7 -  ML {*EVERY;
     4.8 -op THEN;
     4.9 -op THEN';
    4.10 -op oo;
    4.11 -simpset_of;
    4.12 -distinct;
    4.13 -*}
    4.14 -  ML {*
    4.15 -rpair;
    4.16 -map (rpair []) [1,2,3,4];
    4.17 -*}
    4.18 -
    4.19 -
    4.20    ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
    4.21    ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
    4.22  (*use "xmlsrc/mathml.sml"             TODO*)