1.1 --- a/src/Tools/isac/Specify/specify.sml	Tue Jun 21 13:51:04 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/specify.sml	Tue Jun 21 16:04:43 2022 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  *)
     1.5  fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
     1.6      let
     1.7 -      fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
     1.8 +      fun test_d d (i, _, _, _, itm_) = (d = (I_Model.descriptor itm_)) andalso i <> 0
     1.9        fun is_elem itms (_, (d, _)) = 
    1.10          case find_first (test_d d) itms of SOME _ => true | NONE => false
    1.11      in
    1.12 @@ -46,11 +46,11 @@
    1.13        fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
    1.14        fun test_id ids r = member op= ids (#1 (r : O_Model.single))
    1.15        fun test_subset itm (_, _, _, d, ts) = 
    1.16 -        (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
    1.17 +        (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
    1.18        fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
    1.19          | false_and_not_Sup (_, _, false, _, _) = true
    1.20          | false_and_not_Sup _ = false
    1.21 -      val v = if itms = [] then 1 else I_Model.max_vt itms
    1.22 +      val v = if itms = [] then 1 else I_Model.max_variant itms
    1.23        val vors = if v = 0 then oris else filter (testr_vt v) oris
    1.24        val vits =
    1.25          if v = 0
    1.26 @@ -65,7 +65,7 @@
    1.27        else
    1.28          case find_first (test_subset (hd icl)) vors of
    1.29            NONE => raise ERROR "item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
    1.30 -        | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))
    1.31 +        | SOME ori => SOME (I_Model.get_field_term thy ori (hd icl))
    1.32      end
    1.33  
    1.34  
    1.35 @@ -169,7 +169,7 @@
    1.36          I_Model.Add i_single => (*..union old input *)
    1.37  	        let
    1.38  	          val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
    1.39 -            val tac' = I_Model.get_tac m_field (ct, i_model')
    1.40 +            val tac' = I_Model.make_tactic m_field (ct, i_model')
    1.41  	          val  (_, _, _, pt') =  Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
    1.42  	        in
    1.43              ("ok", ([(Tactic.input_from_T tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],