src/HOL/Library/Dlist.thy

--- a/src/HOL/Library/Dlist.thy	Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Jul 12 08:58:13 2010 +0200
@@ -23,7 +23,7 @@
 text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
 
 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
-  [code del]: "Dlist xs = Abs_dlist (remdups xs)"
+  "Dlist xs = Abs_dlist (remdups xs)"
 
 lemma distinct_list_of_dlist [simp]:
   "distinct (list_of_dlist dxs)"