# HG changeset patch
# User berghofe
# Date 1040042591 -3600
# Node ID a9bb54a3cfb7a62d111ef6f789010b460b12d30b
# Parent  021cf00435a903559c65cbbd4aca08b96c71d1ae
Added mk_int and mk_list.

diff -r 021cf00435a9 -r a9bb54a3cfb7 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Dec 16 11:18:35 2002 +0100
+++ b/src/HOL/Main.thy	Mon Dec 16 13:43:11 2002 +0100
@@ -39,7 +39,12 @@
 
   "wfrec"   ("wf'_rec?")
 
-ML {* fun wf_rec f x = f (wf_rec f) x; *}
+ML {*
+fun wf_rec f x = f (wf_rec f) x;
+
+val term_of_list = HOLogic.mk_list;
+val term_of_int = HOLogic.mk_int;
+*}
 
 lemma [code]: "((n::nat) < 0) = False" by simp
 declare less_Suc_eq [code]
diff -r 021cf00435a9 -r a9bb54a3cfb7 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Mon Dec 16 11:18:35 2002 +0100
+++ b/src/HOL/hologic.ML	Mon Dec 16 13:43:11 2002 +0100
@@ -66,6 +66,7 @@
   val mk_nat: int -> term
   val dest_nat: term -> int
   val intT: typ
+  val mk_int: int -> term
   val realT: typ
   val binT: typ
   val pls_const: term
@@ -74,7 +75,8 @@
   val number_of_const: typ -> term
   val int_of: int list -> int
   val dest_binum: term -> int
-  val mk_bin   : int -> term
+  val mk_bin: int -> term
+  val mk_list: ('a -> term) -> typ -> 'a list -> term
 end;
 
 
@@ -271,11 +273,6 @@
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 
-val intT = Type ("IntDef.int", []);
-
-val realT = Type("RealDef.real",[]);
-
-
 (* binary numerals *)
 
 val binT = Type ("Numeral.bin", []);
@@ -316,4 +313,24 @@
       | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
     in term_of (bin_of n) end;
 
+
+(* int *)
+
+val intT = Type ("IntDef.int", []);
+
+fun mk_int i = number_of_const intT $ mk_bin i;
+
+
+(* real *)
+
+val realT = Type("RealDef.real", []);
+
+
+(* list *)
+
+fun mk_list f T [] = Const ("List.list.Nil", Type ("List.list", [T]))
+  | mk_list f T (x :: xs) = Const ("List.list.Cons",
+      T --> Type ("List.list", [T]) --> Type ("List.list", [T])) $ f x $
+        mk_list f T xs;
+
 end;