--- 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", []);