# HG changeset patch
# User nipkow
# Date 1124193264 -7200
# Node ID 051b0897bc983ce7c0d0f45bed696a11595df9c3
# Parent  b0e9462db0b4f42ebccae6766c603becf3573a73
added listT

diff -r b0e9462db0b4 -r 051b0897bc98 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Aug 16 13:42:53 2005 +0200
+++ b/src/HOL/hologic.ML	Tue Aug 16 13:54:24 2005 +0200
@@ -84,6 +84,7 @@
   val dest_binum: term -> IntInf.int
   val mk_bin: IntInf.int -> term
   val bin_of : term -> int list
+  val listT : typ -> typ
   val mk_list: ('a -> term) -> typ -> 'a list -> term
   val dest_list: term -> term list
 end;
@@ -343,9 +344,11 @@
 
 (* list *)
 
-fun mk_list f T [] = Const ("List.list.Nil", Type ("List.list", [T]))
+fun listT T =  Type ("List.list", [T])
+
+fun mk_list f T [] = Const ("List.list.Nil", listT T)
   | mk_list f T (x :: xs) = Const ("List.list.Cons",
-      T --> Type ("List.list", [T]) --> Type ("List.list", [T])) $ f x $
+      T --> listT T --> listT T) $ f x $
         mk_list f T xs;
 
 fun dest_list (Const ("List.list.Nil", _)) = []