Added nil_const and cons_const.

--- a/src/HOL/hologic.ML	Thu Jan 10 19:10:08 2008 +0100
+++ b/src/HOL/hologic.ML	Thu Jan 10 19:10:37 2008 +0100
@@ -110,6 +110,8 @@
   val mk_char: int -> term
   val dest_char: term -> int
   val listT: typ -> typ
+  val nil_const: typ -> term
+  val cons_const: typ -> term
   val mk_list: typ -> term list -> term
   val dest_list: term -> term list
   val stringT: typ
@@ -544,6 +546,12 @@
 
 fun listT T = Type ("List.list", [T]);
 
+fun nil_const T = Const ("List.list.Nil", listT T);
+
+fun cons_const T =
+  let val lT = listT T
+  in Const ("List.list.Cons", T --> lT --> lT) end;
+
 fun mk_list T ts =
   let
     val lT = listT T;