--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Feb 15 12:11:00 2018 +0100
@@ -303,7 +303,7 @@
(* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *)
lemma
- "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
+ "(x, z) \<in> rtrancl (R Un S) \<Longrightarrow> \<exists>y. (x, y) \<in> rtrancl R \<and> (y, z) \<in> rtrancl S"
(*quickcheck[exhaustive, expect = counterexample]*)
oops