src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Sun Oct 16 14:48:00 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sun Oct 16 14:48:00 2011 +0200
@@ -779,8 +779,8 @@
 by (induct n) (simp, simp add: O_assoc [symmetric])
 
 lemma rel_pow_empty:
-  "0 < n ==> ({} :: 'a * 'a => bool) ^^ n = {}"
-by (cases n) auto
+  "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"
+  by (cases n) auto
 
 lemma rtrancl_imp_UN_rel_pow:
   assumes "p \<in> R^*"