changeset 43329 | 84472e198515 |
parent 42247 | 12fe41a92cd5 |
child 45693 | bbd2c7ffc02c |
--- a/src/HOL/Typerep.thy Wed Jun 08 22:16:21 2011 +0200 +++ b/src/HOL/Typerep.thy Thu Jun 09 20:22:22 2011 +0200 @@ -47,7 +47,7 @@ fun add_typerep tyco thy = let val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; - val vs = Name.names Name.context "'a" sorts; + val vs = Name.invent_names Name.context "'a" sorts; val ty = Type (tyco, map TFree vs); val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep}) $ Free ("T", Term.itselfT ty);