1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon Oct 02 12:02:59 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Mon Oct 02 15:39:22 2023 +0200
     1.3 @@ -176,8 +176,8 @@
     1.4             else
     1.5               if pI <> spI 
     1.6  	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth) 
     1.7 -                  else
     1.8 -		                let val pbt = (#model o Problem.from_store ctxt) pI
     1.9 +                  else let
    1.10 +                      val pbt = (#model o Problem.from_store ctxt) pI
    1.11  			                val dI' = #1 (References.select_input ospec spec)
    1.12  			                val oris =
    1.13  			                  if pI = #2 ospec then oris 
    1.14 @@ -186,14 +186,12 @@
    1.15  				              (map (itms2fstr ctxt) probl), meth) end 
    1.16               else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
    1.17  	                then let
    1.18 -                         val pbl_patt = (#model o Problem.from_store ctxt) pI
    1.19 -                         val met = (#model o MethodC.from_store ctxt) mI
    1.20 -		                     val (_, mits) = I_Model.s_make_complete oris
    1.21 -		                       (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (met, pbl_patt)
    1.22 -		                   in if foldl and_ (true, map #3 mits)
    1.23 -		                      then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
    1.24 -		                      else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
    1.25 -		                   end 
    1.26 +		                  val (_, mits) = I_Model.s_make_complete ctxt oris
    1.27 +		                    (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (pI, mI)
    1.28 +		                in if foldl and_ (true, map #3 mits)
    1.29 +		                   then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
    1.30 +		                   else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
    1.31 +		                end 
    1.32                    else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
    1.33  			                  ((#model o Problem.from_store ctxt)
    1.34  			                    (#2 (References.select_input ospec spec)))