1.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Sun Oct 27 12:10:57 2019 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Wed Oct 30 11:02:41 2019 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4  val {srls, pre, prls, ...} = get_met mI;
     1.5  val pres = check_preconds thy prls pre meth |> map snd;
     1.6  val ctxt = ctxt |> insert_assumptions pres;
     1.7 -val (is'''' as Pstate (env'''',_,_,_,_,_), _, sc'''') = init_pstate ctxt meth mI;
     1.8 +val (is'''' as Pstate (env'''',_,_,_,_,_,_), _, sc'''') = init_pstate ctxt meth mI;
     1.9  "~~~~~ fun init_pstate , args:"; val (thy, itms, metID) = (thy, meth, mI)
    1.10      val actuals = itms2args thy metID itms
    1.11  	  val scr as Prog sc = (#scr o get_met) metID
    1.12 @@ -131,7 +131,7 @@
    1.13          val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.14  	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
    1.15  "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), 
    1.16 -	    (Istate.Pstate (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
    1.17 +	    (Istate.Pstate (E,l,rls,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
    1.18  l = [] (* = true*);
    1.19  "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =
    1.20    (thy, ptp, E, [Celem.R], body, NONE, v);