1.1 --- a/test/Tools/isac/Specify/i-model.sml	Mon May 18 11:58:55 2020 +0200
     1.2 +++ b/test/Tools/isac/Specify/i-model.sml	Mon May 18 14:02:54 2020 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4       Specify.by_tactic' "#Given" ct (pt, p);
     1.5  "~~~~~ fun specify_additem , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =
     1.6    ("#Given", ct, (pt, p));
     1.7 -        val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)
     1.8 +        val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
     1.9          val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
    1.10          val cpI = if pI = Problem.id_empty then pI' else pI
    1.11          val cmI = if mI = Method.id_empty then mI' else mI
    1.12 @@ -101,7 +101,7 @@
    1.13  (*+*)then () else error "FINAL I_Model CHANGED";
    1.14  
    1.15  	            val (p, pt') =
    1.16 -	              case Specify_Step.add (make sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
    1.17 +	              case Specify_Step.add (I_Model.get_tac sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
    1.18    	              ((p, Pbl), _, _, pt') => (p, pt')
    1.19  	            val pre = Pre_Conds.check' thy prls where_ pbl'
    1.20  	            val pb = foldl and_ (true, map fst pre)