src/Tools/isac/Specify/p-spec.sml
changeset 60470 dab7b21673ee
parent 60422 6a5f3a2e6d3a
child 60471 37f4a25ec3a9
     1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon Jun 20 11:55:55 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Mon Jun 20 16:58:32 2022 +0200
     1.3 @@ -234,8 +234,9 @@
     1.4                    else
     1.5  		                let val pbt = (#ppc o Problem.from_store) pI
     1.6  			                val dI' = #1 (References.select ospec spec)
     1.7 -			                val oris = if pI = #2 ospec then oris 
     1.8 -				                         else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
     1.9 +			                val oris =
    1.10 +			                  if pI = #2 ospec then oris 
    1.11 +				                else O_Model.init (ThyC.get_theory "Isac_Knowledge") fmz_ pbt(* |> #1*);
    1.12  		                in (Pos.Pbl, appl_adds dI' oris probl pbt 
    1.13  				              (map itms2fstr probl), meth) end 
    1.14               else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)