# HG changeset patch
# User haftmann
# Date 1245566337 -7200
# Node ID 926ebca5a145746255544d43cdcb7046662cd725
# Parent  a00292a5587d58f9b51cb32a52e21c8fbc2e53dc
more appropriate mk_typerep

diff -r a00292a5587d -r 926ebca5a145 src/HOL/Tools/hologic.ML
--- 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", []);