TFL/usyntax.ML
changeset 20071 8f3e1ddb50e6
parent 19046 bc5c6c9b114e
     1.1 --- a/TFL/usyntax.ML	Tue Jul 11 12:16:52 2006 +0200
     1.2 +++ b/TFL/usyntax.ML	Tue Jul 11 12:16:54 2006 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4  
     1.5  fun dest_abs used (a as Abs(s, ty, M)) =
     1.6       let
     1.7 -       val s' = variant used s;
     1.8 +       val s' = Name.variant used s;
     1.9         val v = Free(s', ty);
    1.10       in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
    1.11       end