1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Mon Dec 11 09:24:02 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Mon Dec 11 12:14:28 2023 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4        val pbl = I_Model.init_POS ctxt oris model (* fill in descriptions *)
     1.5        val (pbl, met) = case cas of
     1.6          NONE => (pbl, [])
     1.7 -      | _ => I_Model.s_make_complete ctxt oris (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI)
     1.8 +      | _ => I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
     1.9        val tac_ = Tactic.Model_Problem' (pI, pbl, met)
    1.10        val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
    1.11      in
    1.12 @@ -72,7 +72,7 @@
    1.13        | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
    1.14  	    val thy = if dI' = ThyC.id_empty then dI else dI'
    1.15      in 
    1.16 -      case Refine.problem (ThyC.get_theory ctxt thy) pI (I_Model.OLD_to_POS probl) of
    1.17 +      case Refine.problem (ThyC.get_theory ctxt thy) pI probl of
    1.18  	      NONE => ("failure", ([], [], ptp))
    1.19  	    | SOME (pI, (i_model, prec)) => 
    1.20  	      let 
    1.21 @@ -92,9 +92,8 @@
    1.22        val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
    1.23  	    val (check, (i_model, preconds)) = 
    1.24  	      if pI' = Problem.id_empty andalso pI = Problem.id_empty
    1.25 -	      then (false, (I_Model.OLD_to_POS (I_Model.init model), []))
    1.26 -	      else M_Match.by_i_models ctxt oris
    1.27 -            (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
    1.28 +	      then (false, (I_Model.init_POS ctxt oris model, []))
    1.29 +	      else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
    1.30  	    val (c, pt) =
    1.31  	      case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
    1.32    	      ((_, Pbl), c, _, pt) => (c, pt)
    1.33 @@ -252,7 +251,7 @@
    1.34  	      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
    1.35  				  ([], (dI,pI,mI), hdl, ContextC.empty)
    1.36  	      val pt = update_spec pt [] (dI, pI, mI)
    1.37 -	      val pits = I_Model.init (*Proof_Context.init_global thy*) model
    1.38 +	      val pits = I_Model.init_POS (Proof_Context.init_global thy) [(*o_model*)] model
    1.39  	      val pt = update_pbl pt [] pits
    1.40  	    in ((pt, ([] , Pbl)), []) end
    1.41      else 
    1.42 @@ -264,7 +263,7 @@
    1.43  	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
    1.44  	          ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
    1.45  	        val pt = update_spec pt [] (dI, pI, mI)
    1.46 -	        val mits = I_Model.init (*Proof_Context.init_global thy*) model
    1.47 +	        val mits = I_Model.init_POS (Proof_Context.init_global thy) [(*o_model*)] model
    1.48  	        val pt = update_met pt [] mits
    1.49  	      in ((pt, ([], Met)), []) end
    1.50        else (* new example, pepare for interactive modeling *)