# HG changeset patch
# User haftmann
# Date 1268231362 -3600
# Node ID cfe0accda6e32c682a6f694588c8e894ca85e846
# Parent  564a49e8be44d14234b3f63b28cbd43817cc582e
avoid confusion

diff -r 564a49e8be44 -r cfe0accda6e3 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Wed Mar 10 15:29:21 2010 +0100
+++ b/src/HOL/Library/Dlist.thy	Wed Mar 10 15:29:22 2010 +0100
@@ -123,8 +123,6 @@
   "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
   by (simp add: filter_def)
 
-declare null_def [code] member_def [code] length_def [code] fold_def [code] -- {* explicit is better than implicit *}
-
 
 section {* Implementation of sets by distinct lists -- canonical! *}