1.1 --- a/src/Tools/isac/Specify/input-calchead.sml	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/input-calchead.sml	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  fun cas_input_ ((dI, pI, mI): Spec.T) dtss = (*WN110515 reconsider thy..ctxt*)
     1.5    let
     1.6      val thy = ThyC.get_theory dI
     1.7 -	  val {ppc, ...} = Specify.get_pbt pI
     1.8 +	  val {ppc, ...} = Problem.from_store pI
     1.9  	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
    1.10  	  val its = O_Model.add_id its_
    1.11  	  val pits = map flattup2 its
    1.12 @@ -63,9 +63,9 @@
    1.13        then (pI, mI)
    1.14  		  else
    1.15          case Refine.problem thy pI pits of
    1.16 -			    SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)
    1.17 -			  | NONE => (pI, (hd o #met o Specify.get_pbt) pI)
    1.18 -	  val {ppc, pre, prls, ...} = Specify.get_met mI
    1.19 +			    SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI)
    1.20 +			  | NONE => (pI, (hd o #met o Problem.from_store) pI)
    1.21 +	  val {ppc, pre, prls, ...} = Method.from_store mI
    1.22  	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
    1.23  	  val its = O_Model.add_id its_
    1.24  	  val mits = map flattup2 its
    1.25 @@ -269,35 +269,35 @@
    1.26  	         if dI <> sdI
    1.27  	         then let val its = map (parsitm (ThyC.get_theory dI)) probl;
    1.28  			            val (its, trms) = filter_sep is_Par its;
    1.29 -			            val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
    1.30 +			            val pbt = (#ppc o Problem.from_store) (#2 (Chead.some_spec ospec sspec))
    1.31  		            in (Pos.Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end 
    1.32             else
    1.33               if pI <> spI 
    1.34  	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth) 
    1.35                    else
    1.36 -		                let val pbt = (#ppc o Specify.get_pbt) pI
    1.37 +		                let val pbt = (#ppc o Problem.from_store) pI
    1.38  			                val dI' = #1 (Chead.some_spec ospec spec)
    1.39  			                val oris = if pI = #2 ospec then oris 
    1.40  				                         else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
    1.41  		                in (Pos.Pbl, appl_adds dI' oris probl pbt 
    1.42  				              (map itms2fstr probl), meth) end 
    1.43               else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
    1.44 -	                then let val met = (#ppc o Specify.get_met) mI
    1.45 +	                then let val met = (#ppc o Method.from_store) mI
    1.46  		                     val mits = Chead.complete_metitms oris probl meth met
    1.47  		                   in if foldl and_ (true, map #3 mits)
    1.48  		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) 
    1.49  		                   end 
    1.50                    else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
    1.51 -			                  ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
    1.52 +			                  ((#ppc o Problem.from_store) (#2 (Chead.some_spec ospec spec)))
    1.53  			                  (imodel2fstr imodel), meth)
    1.54  	         val pt = Ctree.update_spec pt p spec;
    1.55           in if pos_ = Pos.Pbl
    1.56 -	          then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
    1.57 +	          then let val {prls,where_,...} = Problem.from_store (#2 (Chead.some_spec ospec spec))
    1.58  		               val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
    1.59  	               in (Ctree.update_pbl pt p pits,
    1.60  		                 (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd) 
    1.61                   end
    1.62 -	           else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
    1.63 +	           else let val {prls,pre,...} = Method.from_store (#3 (Chead.some_spec ospec spec))
    1.64  		                val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
    1.65  	                in (Ctree.update_met pt p mits,
    1.66  		                  (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)