# HG changeset patch
# User blanchet
# Date 1409695583 -7200
# Node ID 414deb2ef328781f7da4e7a28448b4b23d975863
# Parent  2bf3ed0f62cf08e4a3445ede73b5a64b2b1319e2
take out 'x = C' of the simplifier for unit types

diff -r 2bf3ed0f62cf -r 414deb2ef328 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 03 00:06:22 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 03 00:06:23 2014 +0200
@@ -807,7 +807,10 @@
 
 \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
 @{thm list.collapse(1)[no_vars]} \\
-@{thm list.collapse(2)[no_vars]}
+@{thm list.collapse(2)[no_vars]} \\
+(The @{text "[simp]"} attribute is exceptionally omitted for datatypes equipped
+with a single nullary constructor, because a property of the form
+@{prop "x = C"} is not suitable as a simplification rule.)
 
 \item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
 These properties are missing for @{typ "'a list"} because there is only one
@@ -840,8 +843,8 @@
 \end{indentblock}
 
 \noindent
-In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
-attribute.
+In addition, equational versions of @{text t.disc} are registered with the
+@{text "[code]"} attribute.
 *}
 
 
diff -r 2bf3ed0f62cf -r 414deb2ef328 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 00:06:22 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 00:06:23 2014 +0200
@@ -983,7 +983,7 @@
            (case_congN, [case_cong_thm], []),
            (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
            (case_eq_ifN, case_eq_if_thms, []),
-           (collapseN, safe_collapse_thms, simp_attrs),
+           (collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs),
            (discN, flat nontriv_disc_thmss, simp_attrs),
            (discIN, nontriv_discI_thms, []),
            (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),