--- a/src/HOL/Library/Dlist.thy Mon Jul 11 17:22:31 2011 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Jul 11 18:44:58 2011 +0200
@@ -125,6 +125,8 @@
end
+declare equal_dlist_def [code]
+
lemma [code nbe]:
"HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
by (fact equal_refl)