test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml
changeset 59676 6c23dc07c454
parent 59672 1a8ee6c67018
child 59677 b55a25b8ac0c
     1.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Sun Oct 27 12:10:57 2019 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Wed Oct 30 11:02:41 2019 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4     val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
     1.5     val thy' = get_obj g_domID pt p;
     1.6     val thy = assoc_thy thy';
     1.7 -   val (is as Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
     1.8 +   val (is as Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate ctxt itms mI;
     1.9        (*dont take ctxt                   ^^^ from   ^^^^^^^^^^^^^*)
    1.10  
    1.11  (*+*)val (pt, p) = case locatetac tac (pt, pos) of
    1.12 @@ -73,7 +73,7 @@
    1.13  val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.14  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.15  "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
    1.16 -	                               (Pstate (ist as (E,l,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.17 +	                               (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.18  
    1.19  (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
    1.20