1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4    type record = {thy_id: ThyC.id, pbl_id: Problem.id,           (* headline of Problem *)
     1.5      givens: TermC.as_string list, wheres: TermC.as_string list, (* Model.T             *)
     1.6        find: TermC.as_string, relates: TermC.as_string list,
     1.7 -    rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: Method.id}  (* References.T        *)
     1.8 +    rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: MethodC.id}  (* References.T        *)
     1.9  
    1.10  fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
    1.11  
    1.12 @@ -67,7 +67,7 @@
    1.13    Pos.pos' *         (* the position in Ctree              *) 
    1.14    TermC.as_string *  (* the headline shown on Calc.T       *)
    1.15    imodel *           (* the model                          *)
    1.16 -  Pos.pos_ *         (* model belongs to Problem or Method *)
    1.17 +  Pos.pos_ *         (* model belongs to Problem or MethodC *)
    1.18    References.T;      (* into Know_Store                    *)
    1.19  val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
    1.20  
    1.21 @@ -228,7 +228,7 @@
    1.22  		                in (Pos.Pbl, appl_adds dI' oris probl pbt 
    1.23  				              (map itms2fstr probl), meth) end 
    1.24               else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
    1.25 -	                then let val met = (#ppc o Method.from_store) mI
    1.26 +	                then let val met = (#ppc o MethodC.from_store) mI
    1.27  		                     val mits = I_Model.complete oris probl meth met
    1.28  		                   in if foldl and_ (true, map #3 mits)
    1.29  		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) 
    1.30 @@ -243,7 +243,7 @@
    1.31  	               in (Ctree.update_pbl pt p pits,
    1.32  		                 (SpecificationC.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T) 
    1.33                   end
    1.34 -	           else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
    1.35 +	           else let val {prls,pre,...} = MethodC.from_store (#3 (References.select ospec spec))
    1.36  		                val (_, pre) = Pre_Conds.check prls pre mits 0
    1.37  	                in (Ctree.update_met pt p mits,
    1.38  		                  (SpecificationC.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)