1.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Tue Jun 25 10:46:20 2019 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Tue Jun 25 12:48:24 2019 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
     1.5          val thy' = get_obj g_domID pt (par_pblobj pt p);
     1.6  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
     1.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), 
     1.8 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), 
     1.9  	    (Selem.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
    1.10  l = [] (* = true*);
    1.11  "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =