merged

--- a/src/HOL/Library/Dlist.thy	Mon Jul 11 23:15:27 2011 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Jul 11 23:20:40 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)