1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri May 13 14:15:59 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri May 13 17:19:38 2011 +0200
     1.3 @@ -1000,13 +1000,12 @@
     1.4  fun specify_additem sel (ct,_) (p,Met) c pt = 
     1.5      let
     1.6        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
     1.7 -		    probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
     1.8 +		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
     1.9        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.10      (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
    1.11        val cpI = if pI = e_pblID then pI' else pI;
    1.12        val cmI = if mI = e_metID then mI' else mI;
    1.13        val {ppc,pre,prls,...} = get_met cmI;
    1.14 -      val ctxt = get_ctxt pt (p,Met);
    1.15      in case appl_add ctxt sel oris met ppc ct of
    1.16        Add itm (*..union old input *) =>
    1.17  	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
    1.18 @@ -1043,12 +1042,11 @@
    1.19  | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
    1.20      let
    1.21        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.22 -		    probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.23 +		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
    1.24        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.25        val cpI = if pI = e_pblID then pI' else pI;
    1.26        val cmI = if mI = e_metID then mI' else mI;
    1.27        val {ppc,where_,prls,...} = get_pbt cpI;
    1.28 -      val ctxt = get_ctxt pt pos;
    1.29      in case appl_add ctxt sel oris pbl ppc ct of
    1.30        Add itm (*..union old input *) =>
    1.31        (* val Add itm = appl_add thy sel oris pbl ppc ct;
    1.32 @@ -1093,7 +1091,7 @@
    1.33  	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy
    1.34      val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    1.35  			(oris, (dI',pI',mI'),e_term)
    1.36 -      (*val pt = update_env pt [] (SOME (e_istate, ctxt)) FIXME.WN110511*)
    1.37 +      val pt = update_ctxt pt [] ctxt (*FIXME.WN110511*)
    1.38      val {ppc, prls, where_, ...} = get_pbt pI'
    1.39      val (pbl, pre, pb) = ([], [], false)
    1.40    in 
    1.41 @@ -1247,10 +1245,9 @@
    1.42  fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = 
    1.43        let
    1.44          val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
    1.45 -		      probl=pbl,spec=(dI,pI,_), ...}) = get_obj I pt p;
    1.46 +		      probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;
    1.47          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.48          val cpI = if pI = e_pblID then pI' else pI;
    1.49 -        val ctxt = get_ctxt pt (p, Pbl); (*FIXME.WN110511 repair*)
    1.50        in
    1.51          case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
    1.52  	        Add itm (*..union old input *) =>
    1.53 @@ -1275,10 +1272,9 @@
    1.54    | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = 
    1.55        let
    1.56          val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.57 -		      probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.58 +		      probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
    1.59          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.60          val cmI = if mI = e_metID then mI' else mI;
    1.61 -        val ctxt = get_ctxt pt (p,Met); (*FIXME.WN110511 repair*)
    1.62        in 
    1.63          case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
    1.64            Add itm (*..union old input *) =>
    1.65 @@ -1553,7 +1549,7 @@
    1.66  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
    1.67          val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.68  				  (pors, (dI, pI, mI), hdl)
    1.69 -          (* val pt = update_env pt [] (SOME (e_istate, pctxt)) FIXME.WN110511*)
    1.70 +        val pt = update_ctxt pt [] pctxt (* FIXME.WN110511*)
    1.71        in ((pt, ([], Pbl)), 
    1.72          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
    1.73        end;