1.1 --- a/src/Tools/isac/Specify/specify.sml	Wed May 27 16:20:06 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/specify.sml	Thu May 28 12:52:25 2020 +0200
     1.3 @@ -117,19 +117,19 @@
     1.4  (*TODO: unify*)
     1.5  fun find_next_step (pt, (p, p_)) =
     1.6    let
     1.7 -(*OLD*)val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) = 
     1.8 +(*OLD* )val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) = 
     1.9  (*OLD*)  case Ctree.get_obj I pt p of
    1.10  (*OLD*)    pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
    1.11  (*OLD*)	  probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
    1.12  (*OLD*)  | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"
    1.13  (*OLD*)in
    1.14  (*OLD*)  if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin then
    1.15 -(*OLD* )
    1.16 +( *OLD*)
    1.17  (*NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _), probl = pbl,
    1.18  (*NEW*)  spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
    1.19  (*NEW*)in
    1.20  (*NEW*)  if Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin then
    1.21 -( *NEW*)
    1.22 +(*NEW*)
    1.23        case mI' of
    1.24          ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
    1.25        | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))