1.1 Binary file doc-src/isac/master_thesis_template.zip has changed

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Wed May 18 16:06:00 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Thu May 19 19:28:22 2011 +0200
     2.3 @@ -1247,7 +1247,6 @@
     2.4      let val ppobj = get_obj I pt p
     2.5      in is_pblobj ppobj end;
     2.6  
     2.7 -
     2.8  fun delete_result pt (p:pos) =
     2.9      (appl_obj (repl_result (fst (get_obj g_loc pt p), NONE) 
    2.10  			   (e_term,[]) Incomplete) pt p);
    2.11 @@ -1262,12 +1261,8 @@
    2.12      PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch, 
    2.13  	    result=(e_term,[]), ostate=Incomplete};
    2.14  
    2.15 -
    2.16 -(*
    2.17 -fun update_fmz  pt pos x = appl_obj (repl_fmz  x) pt pos;
    2.18 -                                       1.00 not used anymore*)
    2.19 -
    2.20 -(*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
    2.21 +(*FIXME.WN0312 update_X X pos pt -> pt could be chained by o (efficiency?)*)
    2.22 +(*fun update_fmz  pt pos x = appl_obj (repl_fmz  x) pt pos; WN01xx *)
    2.23  fun update_ctxt   pt pos x = appl_obj (repl_ctxt   x) pt pos; (*for use on PblObj, 
    2.24  otherwise use fun generate1; compare fun get_ctxt*)
    2.25  fun update_env    pt pos x = appl_obj (repl_env    x) pt pos;
    2.26 @@ -1282,10 +1277,10 @@
    2.27  fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
    2.28  fun update_tac    pt pos x = appl_obj (repl_tac    x) pt pos;
    2.29  fun update_oris   pt pos x = appl_obj (repl_oris   x) pt pos;
    2.30 -fun update_orispec   pt pos x = appl_obj (repl_orispec   x) pt pos;
    2.31 +fun update_orispec pt pos x = appl_obj (repl_orispec   x) pt pos;
    2.32  
    2.33 -(*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
    2.34 -fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
    2.35 +(*WN050305 for handling cut_tree in cappend_atomic + for testing*)
    2.36 +fun update_loc'   pt pos x = appl_obj (repl_loc    x) pt pos;
    2.37  
    2.38  (*13.8.02: options, because istate is no equalitype any more*)
    2.39  fun get_loc EmptyPtree _ = (e_istate, e_ctxt)

     3.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed May 18 16:06:00 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Thu May 19 19:28:22 2011 +0200
     3.3 @@ -125,7 +125,7 @@
     3.4  		            | UNsafe cs' => ("unsafe-ok", cs')
     3.5  		            | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
     3.6  		                (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
     3.7 -                    (*for SEVER.tacs  user to ask ? *)
     3.8 +                    (*for SEVER.tacs user to ask ? *)
     3.9  	           end
    3.10        end;
    3.11  
    3.12 @@ -403,7 +403,7 @@
    3.13  	    | ("not-applicable",_) => (pt, p)
    3.14  	    | ("end-of-calculation", (_, _, ptp)) => ptp
    3.15  	    | ("failure",_) => error "sys-error";
    3.16 -	  val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
    3.17 +	  val (_, ts) = (*WN101102 TODO: locatetac + step create _same_ (pt,p) ?*)
    3.18  	    (case step p ((pt, e_pos'),[]) of
    3.19  		    ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
    3.20  	    | ("helpless",_) => ("helpless: cannot propose tac", [])
    3.21 @@ -414,8 +414,7 @@
    3.22        case ts of 
    3.23          tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end 
    3.24  		  | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
    3.25 -      (*form output comes from locatetac*)
    3.26 -  in (p:pos', []:NEW, TESTg_form (pt, p), 
    3.27 +  in (p:pos', []:NEW, TESTg_form (pt, p) (*form output comes from locatetac*), 
    3.28  	   (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
    3.29  
    3.30  (*for quick test-print-out, until 'type inout' is removed*)

     4.1 --- a/src/Tools/isac/Interpret/mstools.sml	Wed May 18 16:06:00 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Thu May 19 19:28:22 2011 +0200
     4.3 @@ -960,12 +960,9 @@
     4.4  fun pre2str (b, t) = pair2str(bool2str b, term2str t);
     4.5  fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
     4.6  
     4.7 -(*. check preconditions, return true if all true .*)
     4.8 +(* check preconditions, return true if all true *)
     4.9  fun check_preconds' _ [] _ _ = []  (*empty preconditions are true*)
    4.10    | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) =
    4.11 -(* val (prls, pres, pbl, _) = (prls, where_, probl, 0);
    4.12 -   val (prls, pres, pbl, _) = (prls, pre, itms, mvat);
    4.13 -   *)
    4.14      let val env = mk_env pbl;
    4.15          val pres' = map (subst_atomic_all env) pres;
    4.16      in map (evalprecond prls) pres' end;
    4.17 @@ -1012,6 +1009,7 @@
    4.18    fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt;
    4.19  end
    4.20  
    4.21 +(* transfer information set by Variable.declare_constraints *)
    4.22  fun transfer_from_subproblem ctxt_sub ctxt =
    4.23    insert_assumptions (get_assumptions ctxt_sub) ctxt;
    4.24  

     5.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Wed May 18 16:06:00 2011 +0200
     5.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Thu May 19 19:28:22 2011 +0200
     5.3 @@ -15,7 +15,31 @@
     5.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
     5.5  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
     5.6  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method"*)
     5.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set"*)
     5.8 +val (pt'''', p'''') = (pt, p);
     5.9 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
    5.10 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
    5.11 +val (mI,m) = mk_tac'_ tac;
    5.12 +val Appl m = applicable_in p pt m;
    5.13 +member op = specsteps mI; (*false*)
    5.14 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
    5.15 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
    5.16 +val PblObj {meth, ctxt, ...} = get_obj I pt p;
    5.17 +val thy' = get_obj g_domID pt p;
    5.18 +val thy = assoc_thy thy';
    5.19 +val {srls, pre, prls, ...} = get_met mI;
    5.20 +val pres = check_preconds thy prls pre meth |> map snd;
    5.21 +val ctxt = ctxt |> insert_assumptions pres;
    5.22 +val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy meth mI;
    5.23 +val ini = init_form thy sc env;
    5.24 +val p = lev_dn p;
    5.25 +val SOME t = ini;
    5.26 +val (pos,c,_,pt) = 
    5.27 +		  generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
    5.28 +			    (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
    5.29 +("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), 
    5.30 +		    ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate');
    5.31 +
    5.32 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
    5.33  case nxt of ("Rewrite_Set", _) => ()
    5.34  | _ => error "minisubpbl: Method not started in root-problem";
    5.35  

     6.1 --- a/test/Tools/isac/Minisubpbl/600-postcond.sml	Wed May 18 16:06:00 2011 +0200
     6.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond.sml	Thu May 19 19:28:22 2011 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(* Title:  500-postcond.sml
     6.5 +(* Title:  600-postcond.sml
     6.6     Author: Walther Neuper 1105
     6.7     (c) copyright due to lincense terms.
     6.8  *)

     7.1 --- a/test/Tools/isac/Test_Isac.thy	Wed May 18 16:06:00 2011 +0200
     7.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu May 19 19:28:22 2011 +0200
     7.3 @@ -104,13 +104,6 @@
     7.4    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
     7.5    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
     7.6    use "Interpret/mstools.sml"       (*new 2010*)
     7.7 -ML {*
     7.8 -(*test/../ctree.sml*)
     7.9 -val pt = EmptyPtree;
    7.10 -val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
    7.11 -val ctxt = get_obj g_ctxt pt [];
    7.12 -if is_e_ctxt ctxt then () else error "TODO";
    7.13 -*}
    7.14    use "Interpret/ctree.sml"         (*!...!see(25)*)
    7.15    use "Interpret/ptyps.sml"         (*    *)
    7.16  (*use "Interpret/generate.sml"        new 2011*)
    7.17 @@ -178,6 +171,16 @@
    7.18    ("Test", ["sqroot-test","univariate","equation","test"],
    7.19     ["Test","squ-equ-test-subpbl1"]);
    7.20  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    7.21 +
    7.22 +"=(1)= variables known from root-fmz provide type-inference in further input";
    7.23 +val ctxt = get_ctxt pt p;
    7.24 +val SOME known_x = parseNEW ctxt "x+z+z";
    7.25 +val SOME unknown = parseNEW ctxt "xa+b+c";
    7.26 +if type_of known_x = Type ("RealDef.real",[]) then ()
    7.27 +else error "x+1=2 after start root-pbl wrong type-inference for known_x";
    7.28 +if  type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
    7.29 +else error "x+1=2 after start root-pbl wrong type-inference for unknown";
    7.30 +
    7.31  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.32  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.33  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.34 @@ -186,9 +189,24 @@
    7.35  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.36  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
    7.37  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.38 +*}
    7.39 +ML {*
    7.40 +"=(2)= preconds of (root-)met are known at start of lucas-interpreter";
    7.41 +if get_assumptions_ pt p = [(*str2term "precond_rootmet x"*)] then ((*!!!!!!!!!!!!!!!!*))
    7.42 +else error "x+1=2 after start root-met no precondition";
    7.43  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.44  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
    7.45  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.46 +
    7.47 +"=(3)= variables known from sub-fmz provide type-inference in further input";
    7.48 +val ctxt = get_ctxt pt p;
    7.49 +val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*)
    7.50 +val SOME unknown = parseNEW ctxt "a+b+c";
    7.51 +if type_of known_x = Type ("RealDef.real",[]) then ()
    7.52 +else error "x+1=2 after start root-pbl wrong type-inference for known_x";
    7.53 +if  type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
    7.54 +else error "x+1=2 after start root-pbl wrong type-inference for unknown";
    7.55 +
    7.56  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.57  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.58  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.59 @@ -197,27 +215,137 @@
    7.60  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.61  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
    7.62  val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    7.63 +*}
    7.64 +ML {*
    7.65 +"=(4)= preconds of (sub-)met are known at start of lucas-interpreter";
    7.66 +(*del GOON*)terms2strs (get_assumptions_ pt p);
    7.67 +*}
    7.68 +ML {*
    7.69 +if get_assumptions_ pt p =
    7.70 +  [(*parse_patt @{theory} "matches (?a = ?b) (-1 + x = 0)"*)
    7.71 +   (*, precond-rootmet, precond_submet*)] then ()
    7.72 +else error "x+1=2 after start sub-met no precondition";
    7.73 +*}
    7.74 +ML {*
    7.75  val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    7.76 +
    7.77 +"prep =(5)=: inject assumptions into sub-met: sub_asm_out, sub_asm_local";
    7.78 +val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
    7.79 +val ctxt = insert_assumptions [str2term "x < sub_asm_out", str2term "a < sub_asm_local"] cres;
    7.80 +val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
    7.81 +
    7.82  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
    7.83 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.84 +*}
    7.85 +ML {*
    7.86 +"=(5)= transfer of non-local assumptions from sub-met to root-met";
    7.87 +(*del*)terms2strs (get_assumptions_ pt p);
    7.88 +get_assumptions_ pt p = [(*precond_rootmet, precond_submet, sub_asm_out, sub_res*)];
    7.89 +(*del*)terms2strs (get_assumptions_ pt p);
    7.90 +terms2strs (get_assumptions_ pt p);
    7.91 +*}
    7.92 +ML {*
    7.93 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt=Check_P["sqroot-test","univariate","equation","test"*)
    7.94 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    7.95 +*}
    7.96 +ML {*
    7.97 +"=(6)= assumptions collected during lucas-interpretation for proving postcondition";
    7.98 +get_assumptions_ pt p = [(*precond_rootmet, precond_submet, sub_asm_out, sub_res, root_res*)];
    7.99 +terms2strs (get_assumptions_ pt p);
   7.100  *}
   7.101  
   7.102  ML {*
   7.103 +(*############################################################################*)
   7.104  *}
   7.105  ML {*
   7.106 -val t = str2term "precond_rootmet x";
   7.107 -val SOME (s, t') = eval_precond_rootmet "precond_rootmet_" 0 t @{theory};
   7.108 -term2str t'
   7.109 +(*Minisubplb/500-met-sub-to-root.sml*)
   7.110 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
   7.111 +val (dI',pI',mI') =
   7.112 +   ("Test", ["sqroot-test","univariate","equation","test"],
   7.113 +    ["Test","squ-equ-test-subpbl1"]);
   7.114 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   7.115 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.116 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.117 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.118 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.119 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.120 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.121 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
   7.122 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.123 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.124 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
   7.125 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.126 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.127 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.128 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.129 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.130 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.131 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   7.132 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
   7.133 +val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
   7.134 +get_ctxt pt p |> is_e_ctxt;       (*false*)
   7.135 +val ctxt = get_ctxt pt p; 
   7.136 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
   7.137 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
   7.138 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
   7.139 +get_ctxt pt p |> is_e_ctxt;       (*false*)
   7.140 +val ctxt = get_ctxt pt p; 
   7.141 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
   7.142 +get_loc pt p |> snd |> is_e_ctxt; (*false*)
   7.143 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
   7.144 +val (pt'''', p'''') = (pt, p);
   7.145  *}
   7.146  ML {*
   7.147 +locatetac tac (pt,p)
   7.148  *}
   7.149  ML {*
   7.150 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
   7.151 +val (pt, p) = case locatetac tac (pt,p) of
   7.152 +	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";
   7.153  *}
   7.154  ML {*
   7.155 +show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
   7.156 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
   7.157 +val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
   7.158 +tacis; (*= []*)
   7.159 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
   7.160  *}
   7.161  ML {*
   7.162 -
   7.163 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
   7.164 +val thy' = get_obj g_domID pt (par_pblobj pt p);
   7.165 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
   7.166 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Script (h $ body)), 
   7.167 +	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   7.168 +val ctxt = get_ctxt pt pos
   7.169 +val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
   7.170 +l; (*= [R, R, D, L, R]*)
   7.171 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
   7.172 +                                 (thy, ptp, sc, E, l, Skip_, a, v);
   7.173 +1 < length l; (*true*)
   7.174 +val up = drop_last l;
   7.175 +go up sc; (* = Const ("HOL.Let", *)
   7.176  *}
   7.177 -
   7.178 +ML {*
   7.179 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
   7.180 +                                      (t as Const ("HOL.Let",_) $ _), a, v) =
   7.181 +                            (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
   7.182 +ay = Napp_; (*false*)
   7.183 +val up = drop_last l;
   7.184 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
   7.185 +val i = mk_Free (i, T);
   7.186 +val E = upd_env E (i, v);
   7.187 +body; (*= Const ("Script.Check'_elementwise"*)
   7.188 +"~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
   7.189 +                              (thy, ptp, E, (up@[R,D]), body, a, v);
   7.190 +handle_leaf "next  " th sr E a v t; (*= (NONE, STac (Const ("Script.Check'_elementwise"*)
   7.191 +val (a', STac stac) = handle_leaf "next  " th sr E a v t;
   7.192 +"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.Check'_elementwise",_) $ _ $ 
   7.193 +		(set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);
   7.194 +(*2011 changed ^^^^^   *)
   7.195 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
   7.196 +if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()
   7.197 +else error "Check_elementwise changed; after switch sub-->root-method"
   7.198 +*}
   7.199  end
   7.200  
   7.201  (*=== inhibit exn ?=============================================================