diff -r f38b94549dc8 -r fbe93138e540 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Apr 09 18:00:58 2015 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Apr 09 18:00:59 2015 +0200
@@ -259,15 +259,6 @@
 refute [expect = genuine]
 oops
 
-text {* "The union of transitive closures is equal to the transitive closure of unions." *}
-
-lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
-        \<longrightarrow> trans_closure TP P
-        \<longrightarrow> trans_closure TR R
-        \<longrightarrow> (T x y = (TP x y | TR x y))"
-refute [expect = genuine]
-oops
-
 text {* "Every surjective function is invertible." *}
 
 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"