1.1 --- a/src/Tools/isac/Interpret/solve.sml	Wed May 18 09:45:45 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Wed May 18 10:20:11 2011 +0200
     1.3 @@ -242,11 +242,13 @@
     1.4    | solve (mI,m) (pt, po as (p,p_)) =
     1.5        if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: could be detail, too !!*)
     1.6        then
     1.7 -        let val ((p,p_),ps,f,pt) = 
     1.8 -		      generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 
     1.9 -			      m (e_istate, e_ctxt) (p,p_) pt;
    1.10 +        let
    1.11 +          val ctxt = get_ctxt pt po
    1.12 +          val ((p,p_),ps,f,pt) = 
    1.13 +		        generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 
    1.14 +			        m (e_istate, ctxt) (p,p_) pt;
    1.15  	      in ("no-method-specified", (*Free_Solve*)
    1.16 -	        ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_))))
    1.17 +	        ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, ctxt)))], ps, (pt,(p,p_))))
    1.18          end
    1.19        else
    1.20  	      let 
    1.21 @@ -272,11 +274,10 @@
    1.22  fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
    1.23        let
    1.24          val {srls,ppc,...} = get_met mI;
    1.25 -        val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
    1.26 +        val PblObj{meth=itms,origin=(oris,_,_),probl, ctxt, ...} = get_obj I pt p;
    1.27          val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
    1.28          val thy' = get_obj g_domID pt p;
    1.29          val thy = assoc_thy thy';
    1.30 -        val ctxt = get_ctxt pt pos
    1.31          val (is as ScrState (env,_,_,_,_,_), _, scr) = init_scrstate thy itms mI;
    1.32          val ini = init_form thy scr env;
    1.33        in