src/HOL/Tools/hologic.ML
changeset 31736 926ebca5a145
parent 31463 c5681ed50eab
child 32264 0be31453f698
     1.1 --- a/src/HOL/Tools/hologic.ML	Sun Jun 21 08:38:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Sun Jun 21 08:38:57 2009 +0200
     1.3 @@ -603,8 +603,11 @@
     1.4  
     1.5  val typerepT = Type ("Typerep.typerep", []);
     1.6  
     1.7 -fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
     1.8 -  Term.itselfT T --> typerepT) $ Logic.mk_type T;
     1.9 +fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep",
    1.10 +      literalT --> listT typerepT --> typerepT) $ mk_literal tyco
    1.11 +        $ mk_list typerepT (map mk_typerep Ts)
    1.12 +  | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
    1.13 +      Term.itselfT T --> typerepT) $ Logic.mk_type T;
    1.14  
    1.15  val termT = Type ("Code_Eval.term", []);
    1.16