changeset 44206 | 2b47822868e4 |
parent 39093 | 4abe644fcea5 |
child 45004 | 44adaa6db327 |
1.1 --- a/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 15:38:49 2011 +0200 1.2 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 16:34:49 2011 +0200 1.3 @@ -238,7 +238,7 @@ 1.4 1.5 fun dest_abs used (a as Abs(s, ty, M)) = 1.6 let 1.7 - val s' = Name.variant used s; 1.8 + val s' = singleton (Name.variant_list used) s; 1.9 val v = Free(s', ty); 1.10 in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used) 1.11 end