1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Dec 30 11:16:00 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Jan 15 11:47:38 2020 +0100
     1.3 @@ -218,14 +218,14 @@
     1.4     ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
     1.5  1 < length l (*true*);
     1.6  val up = drop_last l;
     1.7 -  term2str (go up sc);
     1.8 -  (go up sc);
     1.9 -(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
    1.10 +  term2str (at_location up sc);
    1.11 +  (at_location up sc);
    1.12 +(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (at_location up sc)
    1.13        ... ???? ... is correct*)
    1.14  "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
    1.15 -	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
    1.16 +	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (at_location up sc));
    1.17        val l = drop_last l; (*comes from e, goes to Abs*)
    1.18 -      val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
    1.19 +      val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location l sc;
    1.20        val i = mk_Free (i, T);
    1.21        val E = Env.update E (i, v);
    1.22  (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)