1.1 --- a/src/Tools/isac/Specify/specification.sml	Fri Sep 16 12:13:23 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/specification.sml	Mon Sep 26 10:57:53 2022 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    int.modelling                                                       +Cor ++++++Cor      \<down>       \<down>
     1.5                    form.args=             [ id ..... id      , ///////  id ....... id    ] \<down>       \<down>
     1.6                    env =                  [(id, v)..(id, v)  , /////// (id, v)....(id, v)] \<down>       \<down>
     1.7 -  interpret code env = [(id, v)..(id, v),(id, v)..(id, v)  , /////// (id, v)....(id, v)] \<down>       \<down>
     1.8 +  interpret code env = [(id, v)..(id, v), (id, v)..(id, v)  , /////// (id, v)....(id, v)] \<down>       \<down>
     1.9      ..extends env       ^^^^^^^^^^^^^^^^   \<down>                           \<down>   \<down>              \<down>       \<down>
    1.10                                     \<down>       \<down>                           \<down>   \<down>              \<down>       \<down>
    1.11  SubProblem on pos = ([2], _)       \<down>       \<down>                           \<down>   \<down>              \<down>       \<down>
    1.12 @@ -112,12 +112,13 @@
    1.13    | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
    1.14  
    1.15  (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
    1.16 -fun get (pt, (p, Pos.Pbl)) = 
    1.17 +fun get (pt, pos as (p, Pos.Pbl)) = 
    1.18      let
    1.19  	    val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
    1.20  	      Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
    1.21  	    | _ => raise ERROR "get Pbl: uncovered case get_obj"
    1.22 -      val {prls, where_, ...} = Problem.from_store (#2 (References.select_input ospec spec))
    1.23 +      val {prls, where_, ...} =
    1.24 +        Problem.from_store_PIDE (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
    1.25        val (_, pre) = Pre_Conds.check prls where_ probl 0
    1.26      in
    1.27        (is_complete' probl pre spec, Pos.Pbl, hdf', probl, pre, spec)