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