1.1 --- a/src/Tools/isac/Interpret/inform.sml	Sat Mar 19 15:18:10 2011 +0100
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Mar 21 00:32:53 2011 +0100
     1.3 @@ -211,7 +211,7 @@
     1.4  	       val (pI, pits, mI, mits, pre) = cas_input_ spec dtss
     1.5  	       val spec = (dI, pI, mI)
     1.6  	       val (pt,_) = 
     1.7 -		   cappend_problem e_ptree [] e_istate ([], e_spec) 
     1.8 +		   cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) 
     1.9  				   ([], e_spec, hdt)
    1.10  	       val pt = update_spec pt [] spec
    1.11  	       val pt = update_pbl pt [] pits
    1.12 @@ -598,11 +598,11 @@
    1.13      (Rewrite (rule2thm' r), 
    1.14       Rewrite' ("Isac", fst ro, erls, false, 
    1.15  	       rule2thm' r, t, (t', a)),
    1.16 -     (e_pos'(*to be updated before generate tacis!!!*), Uistate))
    1.17 +     (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
    1.18    | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) = 
    1.19      (Rewrite_Set (rule2rls' r), 
    1.20       Rewrite_Set' ("Isac", false, rls, t, (t', a)),
    1.21 -     (e_pos'(*to be updated before generate tacis!!!*), Uistate));
    1.22 +     (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)));
    1.23  
    1.24  (*fo = ifo excluded already in inform*)
    1.25  fun concat_deriv rew_ord erls rules fo ifo =
    1.26 @@ -679,8 +679,8 @@
    1.27  			    ((Subproblem _, _, _)::_) => 
    1.28  			    let val ptp as (pt, (p,_)) = all_modspec ptp
    1.29  				val mI = get_obj g_metID pt p
    1.30 -			    in nxt_solv (Apply_Method' (mI, NONE, e_istate)) 
    1.31 -					e_istate ptp end
    1.32 +			    in nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) 
    1.33 +					(e_istate, e_ctxt) ptp end
    1.34  			  | _ => cs';
    1.35  		in compare_step (tacis, c @ c' @ c'', ptp) ifo end
    1.36      end;