1.1 --- a/src/Tools/isac/Specify/specify-step.sml	Mon Dec 11 16:18:42 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/specify-step.sml	Mon Dec 11 17:26:30 2023 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val check: Tactic.input -> Calc.T -> Applicable.T
     1.6    val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
     1.7 -  val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T_POS
     1.8 +  val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
     1.9  end
    1.10  
    1.11  (**)
    1.12 @@ -50,7 +50,7 @@
    1.13            Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI')
    1.14          | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
    1.15  	      val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
    1.16 -	      val pbl = I_Model.init_POS ctxt o_model model_patt
    1.17 +	      val pbl = I_Model.init ctxt o_model model_patt
    1.18        in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
    1.19    | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
    1.20        let
    1.21 @@ -95,7 +95,7 @@
    1.22          | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
    1.23          val {model, where_, where_rls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
    1.24          val (check, (i_model, preconds)) = if pI' = Problem.id_empty andalso pI = Problem.id_empty
    1.25 -          then (false,  (I_Model.init_POS ctxt oris model, []: (bool * term) list))
    1.26 +          then (false,  (I_Model.init ctxt oris model, []: (bool * term) list))
    1.27            else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
    1.28         in
    1.29           Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (i_model, preconds))))