1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Thu May 28 12:52:25 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Thu May 28 13:24:47 2020 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4      (*WN110515 initialise ctxt again from itms and add preconds*)
     1.5    | by_tactic (Tactic.Specify_Method' (mID, _, _)) (pt,pos as (p, _)) =
     1.6        let
     1.7 -(*OLD*) val (oris, _, _, mI', dI, _, pbl, met, ctxt) = case get_obj I pt p of
     1.8 +(*OLD* ) val (oris, _, _, mI', dI, _, pbl, met, ctxt) = case get_obj I pt p of
     1.9  (*OLD*)   PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
    1.10  (*OLD*)      (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
    1.11  (*OLD*) | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
    1.12 @@ -247,7 +247,7 @@
    1.13  (*OLD*) val itms = hack_until_review_Specify_1 mI' itms (*<<<------------------------------------*)
    1.14  (*OLD*) val (pos, _, _, pt) =
    1.15  (*OLD*)   Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
    1.16 -(*---* )
    1.17 +( *---*)
    1.18  (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
    1.19  (*NEW*)    ...} =Calc.specify_data (pt, pos);
    1.20  (*NEW*) val (dI, _, mID) = References.select o_refs refs;
    1.21 @@ -259,7 +259,7 @@
    1.22  (*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
    1.23  (*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
    1.24  (*NEW*)   (Istate_Def.Uistate, ctxt') (pt, pos)
    1.25 -( *NEW*)in
    1.26 +(*NEW*)in
    1.27          ("ok", ([], [], (pt, pos)))
    1.28        end    
    1.29    | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p)  = Specify.by_tactic' "#Given" ct (pt, p)