1.1 --- a/test/Tools/isac/Knowledge/polyeq.sml	Wed Dec 05 15:29:36 2012 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml	Wed Dec 05 15:56:38 2012 +0100
     1.3 @@ -195,13 +195,13 @@
     1.4  (*locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;
     1.5    WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
     1.6  "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), 
     1.7 -	                                   (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
     1.8 +	                                   (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
     1.9                                     ((thy',srls), m  ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
    1.10  val thy = assoc_thy thy';
    1.11  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
    1.12  (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
    1.13    ... Assoc ... is correct*)
    1.14 -"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
    1.15 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
    1.16     ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
    1.17  1 < length l (*true*);
    1.18  val up = drop_last l;
    1.19 @@ -209,7 +209,7 @@
    1.20    (go up sc);
    1.21  (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
    1.22        ... ???? ... is correct*)
    1.23 -"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Script sc,d)), (is as (E,l,a,v,S,b),ss), 
    1.24 +"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
    1.25  	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
    1.26        val l = drop_last l; (*comes from e, goes to Abs*)
    1.27        val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;