diff -r 07f9732804ad -r f1dfcf8be88d src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/List.thy	Mon Feb 27 09:01:49 2012 +0100
@@ -960,6 +960,8 @@
 
 subsubsection {* @{text set} *}
 
+declare set.simps [code_post]  --"pretty output"
+
 lemma finite_set [iff]: "finite (set xs)"
 by (induct xs) auto