src/Tools/isac/Specify/specification.sml
changeset 60559 aba19e46dd84
parent 60557 0be383bdb883
child 60585 b7071d1dd263
     1.1 --- a/src/Tools/isac/Specify/specification.sml	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/specification.sml	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  	      Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} => (ospec, hdf', spec, probl, ctxt)
     1.5  	    | _ => raise ERROR "get Pbl: uncovered case get_obj"
     1.6        val {prls, where_, ...} =
     1.7 -        Problem.from_store_PIDE (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
     1.8 +        Problem.from_store (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
     1.9        val (_, pre) = Pre_Conds.check prls where_ probl 0
    1.10      in
    1.11        (is_complete' probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
    1.12 @@ -128,7 +128,7 @@
    1.13  		  val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
    1.14  		    Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} => (ospec, hdf', spec, meth, ctxt)
    1.15  		  | _ => raise ERROR "get Met: uncovered case get_obj"
    1.16 -      val {prls, pre, ...} = MethodC.from_store_PIDE ctxt (#3 (References.select_input ospec spec))
    1.17 +      val {prls, pre, ...} = MethodC.from_store ctxt (#3 (References.select_input ospec spec))
    1.18        val (_, pre)  = Pre_Conds.check prls pre meth 0
    1.19      in
    1.20        (is_complete' meth pre spec, Pos.Met, hdf', meth, pre, spec)