# HG changeset patch
# User paulson
# Date 1156524357 -7200
# Node ID e3d2d7b01279671c1b01f7e9ff784743e1c227f3
# Parent  029c4f9dc6f42ffe73373914a61da5d875dcf746
explicit type variables prevent empty sorts

diff -r 029c4f9dc6f4 -r e3d2d7b01279 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Aug 25 18:44:59 2006 +0200
+++ b/src/HOL/Product_Type.thy	Fri Aug 25 18:45:57 2006 +0200
@@ -541,7 +541,8 @@
    b) can lead to nontermination in the presence of split_def
 *)
 lemma split_comp_eq: 
-"(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
+  fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
+  shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
   by (rule ext) auto
 
 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"