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