1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Sat Nov 16 20:38:55 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Nov 19 14:19:44 2019 +0100
     1.3 @@ -199,29 +199,29 @@
     1.4  (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
     1.5  member op = specsteps mI (*false*);
     1.6  (*loc_solve_ (mI,m) ptp;
     1.7 -  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
     1.8 +  WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
     1.9  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
    1.10  (*solve m (pt, pos);
    1.11 -  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
    1.12 +  WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    1.13  "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
    1.14  e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
    1.15          val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.16  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.17  		        val d = e_rls;
    1.18  (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    1.19 -  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
    1.20 +  WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    1.21  "~~~~~ fun locate_input_tactic, args:"; val () = ();
    1.22  (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
    1.23  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
    1.24 -(*WAS val NasApp _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
    1.25 -  ... Assoc ... is correct*)
    1.26 +(*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
    1.27 +  ... Ackn_Tac1 ... is correct*)
    1.28  "~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
    1.29     ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
    1.30  1 < length l (*true*);
    1.31  val up = drop_last l;
    1.32    term2str (go up sc);
    1.33    (go up sc);
    1.34 -(*WAS val Skip1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
    1.35 +(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
    1.36        ... ???? ... is correct*)
    1.37  "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
    1.38  	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
    1.39 @@ -232,8 +232,8 @@
    1.40  (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
    1.41  val [(tac_, mout, ctree, pos', xxx)] = ss;
    1.42  val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
    1.43 -(*WAS val NasApp iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
    1.44 -      ... Assoc ... is correct*)
    1.45 +(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
    1.46 +      ... Ackn_Tac1 ... is correct*)
    1.47  "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
    1.48       ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
    1.49  val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t