1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Nov 07 09:22:05 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Nov 07 10:43:32 2019 +0100
     1.3 @@ -213,17 +213,17 @@
     1.4  "~~~~~ fun locate_input_tactic, args:"; val () = ();
     1.5  (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
     1.6  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
     1.7 -(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
     1.8 +(*WAS val NasApp _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
     1.9    ... Assoc ... is correct*)
    1.10 -"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
    1.11 +"~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
    1.12     ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
    1.13  1 < length l (*true*);
    1.14  val up = drop_last l;
    1.15    term2str (go up sc);
    1.16    (go up sc);
    1.17 -(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
    1.18 +(*WAS val NasNap _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
    1.19        ... ???? ... is correct*)
    1.20 -"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
    1.21 +"~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
    1.22  	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
    1.23        val l = drop_last l; (*comes from e, goes to Abs*)
    1.24        val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
    1.25 @@ -232,9 +232,9 @@
    1.26  (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
    1.27  val [(tac_, mout, ctree, pos', xxx)] = ss;
    1.28  val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
    1.29 -(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
    1.30 +(*WAS val NasApp iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
    1.31        ... Assoc ... is correct*)
    1.32 -"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
    1.33 +"~~~~~ 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.34       ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
    1.35  val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
    1.36               val ctxt = get_ctxt pt (p,p_)