1.1 --- a/src/sml/ME/ctree.sml	Wed Dec 17 10:54:41 2003 +0100
     1.2 +++ b/src/sml/ME/ctree.sml	Thu Dec 18 20:32:07 2003 +0100
     1.3 @@ -258,7 +258,12 @@
     1.4      ((strs2str o (map rta2str)) rtas)^")";
     1.5  
     1.6  
     1.7 -type spec = domID * pblID * metID;
     1.8 +type spec = 
     1.9 +     domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
    1.10 +	      specify (Init_Proof..), nxt_specify_init_calc,
    1.11 +	      assod (.SubProblem...), stac2tac (.SubProblem...)*)
    1.12 +     pblID * 
    1.13 +     metID;
    1.14  fun spec2str ((dom,pbl,met)(*:spec*)) = 
    1.15    "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^ 
    1.16    ", " ^ (strs2str met) ^ ")";
    1.17 @@ -668,7 +673,7 @@
    1.18  	       origin: (ori list) * (*representation from fmz+pbt
    1.19                                    for efficiently adding items in probl, meth*)
    1.20  		       spec *     (*updated by Refine_Tacitly*)
    1.21 -		       term,      (*headform of calc-head*)
    1.22 +		       term,      (*headline of calc-head*)
    1.23  	       spec  : spec,      (*explicitly input + displayed*)
    1.24  	       probl : itm list,  (*itms explicitly input*)
    1.25  	       meth  : itm list,  (*itms automatically added to copy of probl*)
    1.26 @@ -1569,16 +1574,18 @@
    1.27  val e_ptform = Form e_term;
    1.28  val e_ptform' = ModSpec e_ocalhd;
    1.29  
    1.30 -fun pt_model (PblObj {meth,spec,origin=(_,spec',_),...}) Met =
    1.31 +fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
    1.32      let val (_,_,metID) = get_somespec spec spec'
    1.33  	val {prls,pre=where_,...} = get_met metID
    1.34 -	val (head, pre) = head_precond spec' None prls where_ meth 0
    1.35 -    in ModSpec (Met, head, meth, pre, spec) end
    1.36 -  | pt_model (PblObj {probl,spec,origin=(_,spec',_),...}) _(*Frm,Pbl*) =
    1.37 +	val (_, pre) = head_precond spec' None prls where_ meth 0
    1.38 +    in ModSpec (Met, hdl, meth, pre, spec) end
    1.39 +  | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
    1.40 +(* val (PblObj {probl,spec,origin=(_,spec',hdl),...}) = ppobj;
    1.41 +   *)
    1.42      let val (_,pblID,_) = get_somespec spec spec'
    1.43  	val {prls,where_,cas,...} = get_pbt pblID
    1.44 -	val (head, pre) = head_precond spec' cas prls where_ probl 0
    1.45 -    in ModSpec (Pbl, head, probl, pre, spec) end;
    1.46 +	val (_, pre) = head_precond spec' cas prls where_ probl 0
    1.47 +    in ModSpec (Pbl, hdl, probl, pre, spec) end;
    1.48  
    1.49  
    1.50  fun pt_form (PrfObj {form,...}) = Form form