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?!*)