diff -r 8c3eec5812d8 -r ae44f16dcea5 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Feb 16 17:01:40 2016 +0100
+++ b/src/HOL/Library/Dlist.thy	Tue Feb 16 22:28:19 2016 +0100
@@ -326,7 +326,6 @@
 subgoal by(simp add: natLeq_cinfinite)
 subgoal by(rule ordLess_imp_ordLeq)(simp add: finite_iff_ordLess_natLeq[symmetric] set_def)
 subgoal by(rule predicate2I)(transfer; auto simp add: wpull)
-subgoal by(rule refl)
 subgoal by(simp add: set_def)
 done