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