1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Thu Dec 07 11:54:42 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Thu Dec 07 16:14:32 2023 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4        val (pbl, met) = case cas of
     1.5          NONE => (pbl, [])
     1.6        | _ => I_Model.s_make_complete ctxt oris (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI)
     1.7 -      val tac_ = Tactic.Model_Problem' (pI, I_Model.TEST_to_OLD pbl, I_Model.TEST_to_OLD met)
     1.8 +      val tac_ = Tactic.Model_Problem' (pI, pbl, met)
     1.9        val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
    1.10      in
    1.11        ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
    1.12 @@ -74,12 +74,13 @@
    1.13      in 
    1.14        case Refine.problem (ThyC.get_theory ctxt thy) pI probl of
    1.15  	      NONE => ("failure", ([], [], ptp))
    1.16 -	    | SOME rfd => 
    1.17 +	    | SOME (pI, (i_model, prec)) => 
    1.18  	      let 
    1.19 -          val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
    1.20 +          val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' (pI, (I_Model.OLD_to_POS i_model, prec)) )
    1.21 +            (Istate_Def.Uistate, ctxt) (pt, pos)
    1.22  	      in
    1.23 -	        ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd,
    1.24 -            (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
    1.25 +	        ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' (pI, (I_Model.OLD_to_POS i_model, prec)),
    1.26 +            (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
    1.27          end
    1.28      end
    1.29    | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
    1.30 @@ -95,20 +96,20 @@
    1.31  	      else M_Match.by_i_models ctxt oris
    1.32              (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
    1.33  	    val (c, pt) =
    1.34 -	      case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
    1.35 +	      case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
    1.36    	      ((_, Pbl), c, _, pt) => (c, pt)
    1.37    	    | _ => raise ERROR ""
    1.38      in
    1.39 -      ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds))),
    1.40 +      ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, ( i_model, preconds))),
    1.41          (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
    1.42      end
    1.43    | by_tactic_input (Tactic.Specify_Method id) (pt, pos) =
    1.44      let
    1.45        val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
    1.46 -      val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model))
    1.47 +      val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
    1.48          (Istate_Def.Uistate, ctxt) (pt, pos)
    1.49      in
    1.50 -      ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model),
    1.51 +      ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),
    1.52          (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))
    1.53      end    
    1.54    | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
    1.55 @@ -184,7 +185,7 @@
    1.56    | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =
    1.57        let
    1.58          val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
    1.59 -        val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model))
    1.60 +        val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
    1.61            (Istate_Def.Uistate, ctxt) (pt, pos)
    1.62        in
    1.63          ("ok", ([], [], (pt, pos)))