# HG changeset patch
# User wenzelm
# Date 963773664 -7200
# Node ID b78d4246a320631d122ac02d44b2590c9078be3c
# Parent  8b09c29453acf9d9fe8cd9bacd505701026c2302
added is_unitT;
added proper versions of mk_tuple(T), dest_tuple(T) -- unused;

diff -r 8b09c29453ac -r b78d4246a320 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Sun Jul 16 20:53:35 2000 +0200
+++ b/src/HOL/hologic.ML	Sun Jul 16 20:54:24 2000 +0200
@@ -42,6 +42,7 @@
   val mk_binrel: string -> term * term -> term
   val dest_bin: string -> typ -> term -> term * term
   val unitT: typ
+  val is_unitT: typ -> bool
   val unit: term
   val is_unit: term -> bool
   val mk_prodT: typ * typ -> typ
@@ -167,6 +168,9 @@
 
 val unitT = Type ("unit", []);
 
+fun is_unitT (Type ("unit", [])) = true
+  | is_unitT _ = false;
+
 val unit = Const ("()", unitT);
 
 fun is_unit (Const ("()", _)) = true
@@ -213,6 +217,25 @@
 
 
 
+(* proper tuples *)
+
+local  (*currently unused*)
+
+fun mk_tupleT Ts = foldr mk_prodT (Ts, unitT);
+
+fun dest_tupleT (Type ("unit", [])) = []
+  | dest_tupleT (Type ("*", [T, U])) = T :: dest_tupleT U
+  | dest_tupleT T = raise TYPE ("dest_tupleT", [T], []);
+
+fun mk_tuple ts = foldr mk_prod (ts, unit);
+
+fun dest_tuple (Const ("()", _)) = []
+  | dest_tuple (Const ("Pair", _) $ t $ u) = t :: dest_tuple u
+  | dest_tuple t = raise TERM ("dest_tuple", [t]);
+
+in val _ = unit end;
+
+
 (* nat *)
 
 val natT = Type ("nat", []);