split_beta is now declared as monotonicity rule, to allow bounded
quantifiers in introduction rules of inductive predicates.

--- a/src/HOL/Product_Type.thy	Wed May 07 10:56:39 2008 +0200
+++ b/src/HOL/Product_Type.thy	Wed May 07 10:56:40 2008 +0200
@@ -476,7 +476,7 @@
 Addsimprocs [split_beta_proc, split_eta_proc];
 *}
 
-lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
+lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
   by (subst surjective_pairing, rule split_conv)
 
 lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"