# HG changeset patch
# User wenzelm
# Date 1133301139 -3600
# Node ID 83e92f9b32c413f4439a858b192a93c2ce7f8e2f
# Parent  cd217d16c90d7fee88640aa37edc41f8a5c4ac60
added mk_split;

diff -r cd217d16c90d -r 83e92f9b32c4 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Nov 29 19:26:38 2005 +0100
+++ b/src/HOL/hologic.ML	Tue Nov 29 22:52:19 2005 +0100
@@ -59,6 +59,7 @@
   val dest_prod: term -> term * term
   val mk_fst: term -> term
   val mk_snd: term -> term
+  val mk_split: term -> term
   val prodT_factors: typ -> typ list
   val split_const: typ * typ * typ -> term
   val mk_tuple: typ -> term list -> term
@@ -237,13 +238,19 @@
     Const ("snd", pT --> snd (dest_prodT pT)) $ p
   end;
 
+fun split_const (A, B, C) =
+  Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C);
+
+fun mk_split t =
+  (case Term.fastype_of t of
+    T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
+      Const ("split", T --> mk_prodT (A, B) --> C) $ t
+  | _ => raise TERM ("mk_split: bad body type", [t]));
+
 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
 fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
   | prodT_factors T = [T];
 
-fun split_const (Ta, Tb, Tc) =
-    Const ("split", [[Ta, Tb] ---> Tc, mk_prodT (Ta, Tb)] ---> Tc);
-
 (*Makes a nested tuple from a list, following the product type structure*)
 fun mk_tuple (Type ("*", [T1, T2])) tms =
         mk_prod (mk_tuple T1 tms,