src/HOL/Typerep.thy

--- 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);