more appropriate mk_typerep

--- a/src/HOL/Tools/hologic.ML	Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Sun Jun 21 08:38:57 2009 +0200
@@ -603,8 +603,11 @@
 
 val typerepT = Type ("Typerep.typerep", []);
 
-fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
-  Term.itselfT T --> typerepT) $ Logic.mk_type T;
+fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep",
+      literalT --> listT typerepT --> typerepT) $ mk_literal tyco
+        $ mk_list typerepT (map mk_typerep Ts)
+  | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
+      Term.itselfT T --> typerepT) $ Logic.mk_type T;
 
 val termT = Type ("Code_Eval.term", []);