# HG changeset patch
# User berghofe
# Date 1188318239 -7200
# Node ID bbff04c027ec26c45890dc9495f675ebe4d6429d
# Parent  62b96cf2bebbc274cc9b2b64667a16aee011f6d4
Changed "code" attribute of concat_map_singleton to "code unfold".

diff -r 62b96cf2bebb -r bbff04c027ec src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 28 18:21:53 2007 +0200
+++ b/src/HOL/List.thy	Tue Aug 28 18:23:59 2007 +0200
@@ -1004,7 +1004,7 @@
 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
 by (induct xs) auto
 
-lemma concat_map_singleton[simp, code]: "concat(map (%x. [f x]) xs) = map f xs"
+lemma concat_map_singleton[simp, code unfold]: "concat(map (%x. [f x]) xs) = map f xs"
 by (induct xs) auto
 
 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"