1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Fri Sep 16 12:13:23 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Mon Sep 26 10:57:53 2022 +0200
     1.3 @@ -220,19 +220,21 @@
     1.4  		      spec = sspec as (sdI, spI, smI), probl, meth, ...}
     1.5          => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
     1.6        | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
     1.7 +      val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)
     1.8      in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf)) 
     1.9         else        (*hacked WN0602 ~~~            ~~~~~~~~~,   ..dropped !*)
    1.10           let val (pos_, pits, mits) = 
    1.11  	         if dI <> sdI
    1.12  	         then let val its = map (parsitm (ThyC.get_theory dI)) probl;
    1.13  			            val (its, trms) = filter_sep is_Par its;
    1.14 -			            val pbt = (#ppc o Problem.from_store) (#2 (References.select_input ospec sspec))
    1.15 +			            val pbt =
    1.16 +			              (#ppc o Problem.from_store_PIDE ctxt) (#2 (References.select_input ospec sspec))
    1.17  		            in (Pos.Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end 
    1.18             else
    1.19               if pI <> spI 
    1.20  	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth) 
    1.21                    else
    1.22 -		                let val pbt = (#ppc o Problem.from_store) pI
    1.23 +		                let val pbt = (#ppc o Problem.from_store_PIDE ctxt) pI
    1.24  			                val dI' = #1 (References.select_input ospec spec)
    1.25  			                val oris =
    1.26  			                  if pI = #2 ospec then oris 
    1.27 @@ -246,11 +248,11 @@
    1.28  		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) 
    1.29  		                   end 
    1.30                    else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
    1.31 -			                  ((#ppc o Problem.from_store) (#2 (References.select_input ospec spec)))
    1.32 +			                  ((#ppc o Problem.from_store_PIDE ctxt) (#2 (References.select_input ospec spec)))
    1.33  			                  (imodel2fstr imodel), meth)
    1.34  	         val pt = Ctree.update_spec pt p spec;
    1.35           in if pos_ = Pos.Pbl
    1.36 -	          then let val {prls,where_,...} = Problem.from_store (#2 (References.select_input ospec spec))
    1.37 +	          then let val {prls,where_,...} = Problem.from_store_PIDE ctxt (#2 (References.select_input ospec spec))
    1.38  		               val (_, pre) = Pre_Conds.check prls where_ pits 0
    1.39  	               in (Ctree.update_pbl pt p pits,
    1.40  		                 (SpecificationC.is_complete' pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)