1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Mon Dec 11 16:18:42 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Mon Dec 11 17:26:30 2023 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4        | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
     1.5        val (_, pI, mI) = References.select_input ospec spec
     1.6        val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
     1.7 -      val pbl = I_Model.init_POS ctxt oris model (* fill in descriptions *)
     1.8 +      val pbl = I_Model.init ctxt oris model (* fill in descriptions *)
     1.9        val (pbl, met) = case cas of
    1.10          NONE => (pbl, [])
    1.11        | _ => I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
    1.12 @@ -92,7 +92,7 @@
    1.13        val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
    1.14  	    val (check, (i_model, preconds)) = 
    1.15  	      if pI' = Problem.id_empty andalso pI = Problem.id_empty
    1.16 -	      then (false, (I_Model.init_POS ctxt oris model, []))
    1.17 +	      then (false, (I_Model.init ctxt oris model, []))
    1.18  	      else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
    1.19  	    val (c, pt) =
    1.20  	      case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
    1.21 @@ -251,7 +251,7 @@
    1.22  	      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
    1.23  				  ([], (dI,pI,mI), hdl, ContextC.empty)
    1.24  	      val pt = update_spec pt [] (dI, pI, mI)
    1.25 -	      val pits = I_Model.init_POS (Proof_Context.init_global thy) [(*o_model*)] model
    1.26 +	      val pits = I_Model.init (Proof_Context.init_global thy) [(*o_model*)] model
    1.27  	      val pt = update_pbl pt [] pits
    1.28  	    in ((pt, ([] , Pbl)), []) end
    1.29      else 
    1.30 @@ -263,7 +263,7 @@
    1.31  	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
    1.32  	          ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
    1.33  	        val pt = update_spec pt [] (dI, pI, mI)
    1.34 -	        val mits = I_Model.init_POS (Proof_Context.init_global thy) [(*o_model*)] model
    1.35 +	        val mits = I_Model.init (Proof_Context.init_global thy) [(*o_model*)] model
    1.36  	        val pt = update_met pt [] mits
    1.37  	      in ((pt, ([], Met)), []) end
    1.38        else (* new example, pepare for interactive modeling *)