intermed. ctxt ..: extended PblObj with ctxt decompose-isar
authorWalther Neuper <neuper@ist.tugraz.at>
Fri, 13 May 2011 11:45:07 +0200
branchdecompose-isar
changeset 419880a13bda82a57
parent 41987 f304fe86b45a
child 41989 235f3990c9b7
intermed. ctxt ..: extended PblObj with ctxt

ctxt is for the specify phase. For this purpose ...
...(1) re-using PblObj{env, ...} led to conflict with init_form,
...(2) re-using PblObj{loc = (_, Some (_, ctxt)), ...} led to another conflict,
which could not be traced due to the unstable situation of the system.

the system is in unstable state of development because:
# update 2002 to 2009-2 checked by few tests (only x+1=2, Frontend/interface.sml)
# MLe started work on "parse ctxt" before update 2009-2 to 2011 was done
# so MLe started with too little tests (not even x+1=2 went through)
# HOL.Let, ...,Pair were detected during MLe's work

since the above conflicts cannot be traced sufficiently,
PblObj{ctxt, ...} is added as a save way, which might be removed later.

TODO: remove ctxt from PblObj{env = SOME (istate, ctxt), ...} again,
which was introduced for (1).
src/Tools/isac/Interpret/calchead.sml
src/Tools/isac/Interpret/ctree.sml
src/Tools/isac/Interpret/inform.sml
src/Tools/isac/Interpret/mathengine.sml
     1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri May 13 10:26:44 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri May 13 11:45:07 2011 +0200
     1.3 @@ -1000,7 +1000,7 @@
     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),...}) = 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 @@ -1043,7 +1043,7 @@
    1.13  | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
    1.14      let
    1.15        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.16 -		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.17 +		    probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.18        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.19        val cpI = if pI = e_pblID then pI' else pI;
    1.20        val cmI = if mI = e_metID then mI' else mI;
    1.21 @@ -1113,7 +1113,7 @@
    1.22      (*ONLY for STARTING modeling phase*)
    1.23    | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
    1.24        let 
    1.25 -        val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) = get_obj I pt p
    1.26 +        val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ...}) = get_obj I pt p
    1.27          val thy' = if dI = e_domID then dI' else dI
    1.28          val thy = assoc_thy thy'
    1.29          val {ppc,prls,where_,...} = get_pbt pI'
    1.30 @@ -1156,8 +1156,6 @@
    1.31    | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
    1.32    let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI), 
    1.33  		   meth=met, ...}) = get_obj I pt p;
    1.34 -    (*val pt = update_pbl pt p itms;
    1.35 -    val pt = update_pblID pt p pI;*)
    1.36      val thy = assoc_thy dI
    1.37      val ((p,Pbl),_,_,pt)= 
    1.38  	generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
    1.39 @@ -1208,7 +1206,7 @@
    1.40      let val p_ = case p_ of Met => Met | _ => Pbl
    1.41        val thy = assoc_thy domID;
    1.42        val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
    1.43 -		  probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.44 +		    probl=pbl, spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.45        val mppc = case p_ of Met => met | _ => pbl;
    1.46        val cpI = if pI = e_pblID then pI' else pI;
    1.47        val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
    1.48 @@ -1249,7 +1247,7 @@
    1.49  fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = 
    1.50        let
    1.51          val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
    1.52 -		      probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
    1.53 +		      probl=pbl,spec=(dI,pI,_), ...}) = get_obj I pt p;
    1.54          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.55          val cpI = if pI = e_pblID then pI' else pI;
    1.56          val ctxt = get_ctxt pt (p, Pbl); (*FIXME.WN110511 repair*)
    1.57 @@ -1277,7 +1275,7 @@
    1.58    | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = 
    1.59        let
    1.60          val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.61 -		      probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.62 +		      probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.63          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.64          val cmI = if mI = e_metID then mI' else mI;
    1.65          val ctxt = get_ctxt pt (p,Met); (*FIXME.WN110511 repair*)
    1.66 @@ -1453,7 +1451,8 @@
    1.67      FIXME.WN.8.03: application of several mIDs to SAME model?*)
    1.68    | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) = 
    1.69        let
    1.70 -        val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), meth=met, ...}) = get_obj I pt p;
    1.71 +        val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), 
    1.72 +          meth=met, ...}) = get_obj I pt p;
    1.73          val {ppc,pre,prls,...} = get_met mID
    1.74          val thy = assoc_thy dI
    1.75          val oris = add_field' thy ppc oris;
    1.76 @@ -1719,7 +1718,7 @@
    1.77      let val _= if p_ <> Pbl 
    1.78  	       then tracing("###complete_mod: only impl.for Pbl, called with "^
    1.79  			    pos'2str pos) else ()
    1.80 -	val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
    1.81 +	val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =
    1.82  	    get_obj I pt p
    1.83  	val (dI,pI,mI) = some_spec ospec spec
    1.84  	val mpc = (#ppc o get_met) mI
    1.85 @@ -2003,7 +2002,7 @@
    1.86      in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
    1.87  | get_ocalhd (pt, pos' as (p,Met):pos') = 
    1.88      let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 
    1.89 -		    spec, meth,...} = 
    1.90 +		    spec, meth, ...} = 
    1.91  	    get_obj I pt p
    1.92  	val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
    1.93  	val pre = check_preconds (assoc_thy"Isac") prls pre meth
     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Fri May 13 10:26:44 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Fri May 13 11:45:07 2011 +0200
     2.3 @@ -751,13 +751,15 @@
     2.4  	    spec  : spec,             (* explicitly input *)
     2.5  	    probl : itm list,         (* itms explicitly input *)
     2.6  	    meth  : itm list,         (* itms automatically added to copy of probl *)
     2.7 +      ctxt  : Proof.context,    (* WN110513 introduced to avoid [*] [**]*)
     2.8  	    env   : (istate * Proof.context) option,
     2.9                                  (* istate only for initac in script
    2.10                                     context for specify phase on this node NO..
    2.11  ..NO: this conflicts with init_form/initac: see Apply_Method without init_form
    2.12  in fun step. Replaced by hack FIXME.WN110511 fun update_pbl_ctxt, see [*] below *)
    2.13  	    loc   : (istate * Proof.context) option * (istate * (* like PrfObj *)
    2.14 -                Proof.context) option, (* for spec-phase [*] *)                               
    2.15 +                Proof.context) option, (* for spec-phase [*], NO..
    2.16 +..NO: raises errors not tracable on WN110513 [**]*)                               
    2.17  	    branch: branch,           (* like PrfObj *)
    2.18  	    result: term * term list, (* like PrfObj *)
    2.19  	    ostate: ostate};          (* like PrfObj *)
    2.20 @@ -777,10 +779,10 @@
    2.21  
    2.22  fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
    2.23    {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
    2.24 -fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,
    2.25 -			loc,branch,result,ostate}) =
    2.26 -  {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
    2.27 -   env=env,loc=loc,branch=branch,result=result,ostate=ostate};
    2.28 +fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt,
    2.29 +      env,loc,branch,result,ostate}) =
    2.30 +        {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,ctxt=ctxt,
    2.31 +         env=env,loc=loc,branch=branch,result=result,ostate=ostate};
    2.32  fun is_prfobj (PrfObj _) = true
    2.33    | is_prfobj _ =false;
    2.34  (*val is_prfobj' = get_obj is_prfobj; *)
    2.35 @@ -1108,41 +1110,41 @@
    2.36  	    branch=branch,result=result,ostate=ostate}
    2.37    | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
    2.38  fun repl_pbl x    (PblObj {cell=cell,origin=origin,fmz=fmz,
    2.39 -			   spec=spec,probl=_,meth=meth,env=env,loc=loc,
    2.40 +			   spec=spec,probl=_,meth=meth,ctxt=ctxt,env=env,loc=loc,
    2.41  			   branch=branch,result=result,ostate=ostate}) =
    2.42    PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
    2.43 -	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.44 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.45    | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
    2.46  fun repl_met x    (PblObj {cell=cell,origin=origin,fmz=fmz,
    2.47 -			   spec=spec,probl=probl,meth=_,env=env,loc=loc,
    2.48 +			   spec=spec,probl=probl,meth=_,ctxt=ctxt,env=env,loc=loc,
    2.49  			   branch=branch,result=result,ostate=ostate}) =
    2.50    PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
    2.51 -	  meth= x,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.52 +	  meth= x,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.53    | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
    2.54  
    2.55  fun repl_spec  x    (PblObj {cell=cell,origin=origin,fmz=fmz,
    2.56 -			   spec= _,probl=probl,meth=meth,env=env,loc=loc,
    2.57 +			   spec= _,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
    2.58  			   branch=branch,result=result,ostate=ostate}) =
    2.59    PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
    2.60 -	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.61 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.62    | repl_spec  _ _ = raise PTREE "repl_domID takes no PrfObj";
    2.63  fun repl_domID x    (PblObj {cell=cell,origin=origin,fmz=fmz,
    2.64 -			   spec=(_,p,m),probl=probl,meth=meth,env=env,loc=loc,
    2.65 +			   spec=(_,p,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
    2.66  			   branch=branch,result=result,ostate=ostate}) =
    2.67    PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
    2.68 -	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.69 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.70    | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
    2.71  fun repl_pblID x    (PblObj {cell=cell,origin=origin,fmz=fmz,
    2.72 -			   spec=(d,_,m),probl=probl,meth=meth,env=env,loc=loc,
    2.73 +			   spec=(d,_,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
    2.74  			   branch=branch,result=result,ostate=ostate}) =
    2.75    PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
    2.76 -	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.77 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.78    | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
    2.79  fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
    2.80 -			   spec=(d,p,_),probl=probl,meth=meth,env=env,loc=loc,
    2.81 +			   spec=(d,p,_),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
    2.82  			   branch=branch,result=result,ostate=ostate}) =
    2.83    PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
    2.84 -	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.85 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
    2.86    | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
    2.87  
    2.88  fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
    2.89 @@ -1150,10 +1152,10 @@
    2.90      PrfObj {cell=cell,form=form,tac=tac,loc= l,
    2.91  	    branch=branch,result = f',ostate = s}
    2.92    | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
    2.93 -			     spec=spec,probl=probl,meth=meth,env=env,loc=_,
    2.94 +			     spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=_,
    2.95  			     branch=branch,result= _ ,ostate= _}) =
    2.96      PblObj {cell=cell,origin=origin,fmz=fmz,
    2.97 -	    spec=spec,probl=probl,meth=meth,env=env,loc= l,
    2.98 +	    spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc= l,
    2.99  	    branch=branch,result= f',ostate= s};
   2.100  
   2.101  fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
   2.102 @@ -1163,10 +1165,10 @@
   2.103    | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
   2.104  
   2.105  fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
   2.106 -			   spec=spec,probl=probl,meth=meth,env=env,loc=loc,
   2.107 +			   spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
   2.108  			   branch= _,result=result,ostate=ostate}) =
   2.109    PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
   2.110 -	  meth=meth,env=env,loc=loc,branch= b,result=result,ostate=ostate}
   2.111 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch= b,result=result,ostate=ostate}
   2.112    | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
   2.113  			  branch= _,result=result,ostate=ostate}) =
   2.114      PrfObj {cell=cell,form=form,tac=tac,loc=loc,
   2.115 @@ -1174,52 +1176,38 @@
   2.116  
   2.117  fun repl_env e
   2.118    (PblObj {cell=cell,origin=origin,fmz=fmz,
   2.119 -	   spec=spec,probl=probl,meth=meth,env=_,loc=loc,
   2.120 +	   spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=_,loc=loc,
   2.121  	   branch=branch,result=result,ostate=ostate}) =
   2.122    PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
   2.123 -	  meth=meth,env=e,loc=loc,branch=branch,
   2.124 +	  meth=meth,ctxt=ctxt,env=e,loc=loc,branch=branch,
   2.125  	  result=result,ostate=ostate}
   2.126    | repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
   2.127  
   2.128  fun repl_oris oris
   2.129    (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
   2.130 -	   spec=spec,probl=probl,meth=meth,env=env,loc=loc,
   2.131 +	   spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
   2.132  	   branch=branch,result=result,ostate=ostate}) =
   2.133    PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
   2.134 -	  meth=meth,env=env,loc=loc,branch=branch,
   2.135 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
   2.136  	  result=result,ostate=ostate}
   2.137    | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
   2.138  fun repl_orispec spe
   2.139    (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
   2.140 -	   spec=spec,probl=probl,meth=meth,env=env,loc=loc,
   2.141 +	   spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
   2.142  	   branch=branch,result=result,ostate=ostate}) =
   2.143    PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
   2.144 -	  meth=meth,env=env,loc=loc,branch=branch,
   2.145 +	  meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
   2.146  	  result=result,ostate=ostate}
   2.147    | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
   2.148  
   2.149 -fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,env=env,
   2.150 -    loc=_,branch=branch,result=result,ostate=ostate}) =
   2.151 -       PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,env=env,
   2.152 -         loc=l,branch=branch,result=result,ostate=ostate}
   2.153 +fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
   2.154 +    ctxt=ctxt,env=env,loc=_,branch=branch,result=result,ostate=ostate}) =
   2.155 +       PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
   2.156 +         ctxt=ctxt,env=env,loc=l,branch=branch,result=result,ostate=ostate}
   2.157    | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,
   2.158      loc=_,branch=branch,result=result,ostate=ostate}) =
   2.159         PrfObj {cell=cell,form=form,tac=tac,
   2.160         loc= l,branch=branch,result=result,ostate=ostate};
   2.161 -(*
   2.162 -fun uni__cid cell' 
   2.163 -  (PblObj {cell=cell,origin=origin,fmz=fmz,
   2.164 -	   spec=spec,probl=probl,meth=meth,env=env,loc=loc,
   2.165 -	   branch=branch,result=result,ostate=ostate}) =
   2.166 -  PblObj {cell=cell union cell',origin=origin,fmz=fmz,spec=spec,probl=probl,
   2.167 -	  meth=meth,env=env,loc=loc,branch=branch,
   2.168 -	  result=result,ostate=ostate}
   2.169 -  | uni__cid cell'
   2.170 -  (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
   2.171 -	   branch=branch,result=result,ostate=ostate}) =
   2.172 -  PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,
   2.173 -	  branch=branch,result=result,ostate=ostate};
   2.174 -*)
   2.175  
   2.176  (*WN050219 put here for interpreting code for cut_tree below...*)
   2.177  type ocalhd =
   2.178 @@ -1268,9 +1256,9 @@
   2.179  			   (e_term,[]) Incomplete) pt p);
   2.180  
   2.181  fun del_res (PblObj {cell, fmz, origin, spec, probl, meth, 
   2.182 -		     env, loc=(l1,_), branch, result, ostate}) =
   2.183 +		     ctxt, env, loc=(l1,_), branch, result, ostate}) =
   2.184      PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
   2.185 -	    env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]), 
   2.186 +	    ctxt=ctxt,env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]), 
   2.187  	    ostate=Incomplete}
   2.188  
   2.189    | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
   2.190 @@ -2085,6 +2073,7 @@
   2.191  		spec  = empty_spec,
   2.192  		probl = []:itm list,
   2.193  		meth  = []:itm list,
   2.194 +    ctxt  = e_ctxt,
   2.195  		env   = NONE,
   2.196  		loc   = (SOME l, NONE),
   2.197  		branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
   2.198 @@ -2100,6 +2089,7 @@
   2.199  	   spec  = empty_spec,
   2.200  	   probl = []:itm list,
   2.201  	   meth  = []:itm list,
   2.202 +     ctxt  = e_ctxt,
   2.203  	   env   = NONE,
   2.204  	   loc   = (SOME l, NONE),
   2.205  	   branch= TransitiveB,
   2.206 @@ -2117,6 +2107,6 @@
   2.207  
   2.208  (*.get the theory explicitly specified for the rootpbl;
   2.209     thus use this function _after_ finishing specification.*)
   2.210 -fun rootthy (Nd (PblObj {spec=(thyID, _, _),...}, _)) = assoc_thy thyID
   2.211 +fun rootthy (Nd (PblObj {spec=(thyID, _, _), ...}, _)) = assoc_thy thyID
   2.212    | rootthy _ = error "rootthy";
   2.213  
     3.1 --- a/src/Tools/isac/Interpret/inform.sml	Fri May 13 10:26:44 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/inform.sml	Fri May 13 11:45:07 2011 +0200
     3.3 @@ -405,7 +405,7 @@
     3.4  (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
     3.5  fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) =
     3.6      let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 
     3.7 -		      spec = sspec as (sdI,spI,smI), probl, meth,...} = get_obj I pt p;
     3.8 +		      spec = sspec as (sdI,spI,smI), probl, meth, ...} = get_obj I pt p;
     3.9      in if is_casinput hdf fmz then the (cas_input (str2term hdf)) 
    3.10         else        (*hacked WN0602 ~~~            ~~~~~~~~~,   ..dropped !*)
    3.11           let val (pos_, pits, mits) = 
     4.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Fri May 13 10:26:44 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Fri May 13 11:45:07 2011 +0200
     4.3 @@ -133,7 +133,7 @@
     4.4    may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
     4.5  fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
     4.6    let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
     4.7 -			  probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
     4.8 +			  probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
     4.9    in 
    4.10      if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
    4.11      then