1.1 --- a/src/Tools/isac/Specify/specify-step.sml	Thu Dec 07 16:14:32 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/specify-step.sml	Thu Dec 07 17:16:22 2023 +0100
     1.3 @@ -60,14 +60,14 @@
     1.4            | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
     1.5        	val thy = if dI' = ThyC.id_empty then dI else dI';
     1.6        in
     1.7 -        case Refine.problem (ThyC.get_theory ctxt thy) pI itms of
     1.8 +        case Refine.problem (ThyC.get_theory ctxt thy) pI (I_Model.OLD_to_POS itms) of
     1.9            NONE => Applicable.No
    1.10              (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
    1.11  	      | SOME (pI', (i_model, prec)) =>
    1.12        	   if pI' = pI
    1.13        	   then Applicable.No
    1.14        	     (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
    1.15 -      	   else Applicable.Yes (Tactic.Refine_Problem' (pI', (I_Model.OLD_to_POS i_model, prec)))
    1.16 +      	   else Applicable.Yes (Tactic.Refine_Problem' (pI', (i_model, prec)))
    1.17      end
    1.18    | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
    1.19       let