1.1 --- a/src/Tools/isac/Specify/specification.sml	Mon Dec 11 09:24:02 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/specification.sml	Mon Dec 11 12:14:28 2023 +0100
     1.3 @@ -100,8 +100,7 @@
     1.4      | _ => raise ERROR "SpecificationC.is_complete only with PblObj"
     1.5      val (_, pbl_id, met_id) = References.select_input o_spec spec
     1.6    in
     1.7 -    I_Model.s_are_complete ctxt oris
     1.8 -        (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pbl_id, met_id)
     1.9 +    I_Model.s_are_complete ctxt oris (probl, itms) (pbl_id, met_id)
    1.10    end
    1.11  
    1.12  (** handle acces to Ctree **)
    1.13 @@ -109,7 +108,7 @@
    1.14  fun get_data (pt, (p, _)) =
    1.15    case Ctree.get_obj I pt p of
    1.16      (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
    1.17 -      => (I_Model.OLD_to_POS meth, oris, (dI', pI', mI'), I_Model.OLD_to_POS probl, (dI, pI, mI), ctxt)
    1.18 +      => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
    1.19    | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
    1.20  
    1.21  (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
    1.22 @@ -117,7 +116,7 @@
    1.23      let
    1.24  	    val (ospec, hdf', spec, probl, ctxt) = case Ctree.get_obj I pt p of
    1.25  	      Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} =>
    1.26 -	        (ospec, hdf', spec, I_Model.OLD_to_POS probl, ctxt)
    1.27 +	        (ospec, hdf', spec, probl, ctxt)
    1.28  	    | _ => raise ERROR "get Pbl: uncovered case get_obj"
    1.29        val {where_rls, where_, model, ...} =
    1.30          Problem.from_store ctxt (#2 (References.select_input ospec spec))
    1.31 @@ -130,7 +129,7 @@
    1.32      let
    1.33  		  val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
    1.34  		    Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} =>
    1.35 -		      (ospec, hdf', spec, I_Model.OLD_to_POS meth, ctxt)
    1.36 +		      (ospec, hdf', spec, meth, ctxt)
    1.37  		  | _ => raise ERROR "get Met: uncovered case get_obj"
    1.38        val {where_rls, where_, model, ...} =
    1.39          MethodC.from_store ctxt (#3 (References.select_input ospec spec))