1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Fri Aug 04 23:07:04 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Tue Aug 15 12:22:49 2023 +0200
     1.3 @@ -198,17 +198,31 @@
     1.4           in if pos_ = Pos.Pbl
     1.5  	          then 
     1.6  	            let 
     1.7 +(*T_TESTold* )
     1.8  	              val {where_rls, where_,...} = Problem.from_store ctxt
     1.9  	                (#2 (References.select_input ospec spec))
    1.10  		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
    1.11 +( *T_TEST**)
    1.12 +	              val {where_rls, where_, model, ...} = Problem.from_store ctxt
    1.13 +	                (#2 (References.select_input ospec spec))
    1.14 +		            val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
    1.15 +		              (model, I_Model.OLD_to_TEST pits)
    1.16 +(*T_TESTnew*)
    1.17  	            in (Ctree.update_pbl pt p pits,
    1.18  		                 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec)) 
    1.19                end
    1.20  	          else 
    1.21  	            let 
    1.22 +(*T_TESTold* )
    1.23  	              val {where_rls,where_,...} = MethodC.from_store ctxt 
    1.24  	                (#3 (References.select_input ospec spec))
    1.25  		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
    1.26 +( *T_TEST**)
    1.27 +	              val {where_rls,where_, model, ...} = MethodC.from_store ctxt 
    1.28 +	                (#3 (References.select_input ospec spec))
    1.29 +		            val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
    1.30 +		              (model, I_Model.OLD_to_TEST mits)
    1.31 +(*T_TESTnew*)
    1.32  	            in (Ctree.update_met pt p mits,
    1.33  		                  (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
    1.34                end