# HG changeset patch
# User berghofe
# Date 1199988637 -3600
# Node ID 5dcc3c25792229721c4b6eb13722c13c4b48c3a6
# Parent  7753e0d81b7a8a3278fd0a7633ab193a45750dd4
Added nil_const and cons_const.

diff -r 7753e0d81b7a -r 5dcc3c257922 src/HOL/hologic.ML
--- 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;