--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100
@@ -36,7 +36,6 @@
val discN = "disc"
val disc_iffN = "disc_iff"
val excludeN = "exclude"
-val nchotomyN = "nchotomy"
val selN = "sel"
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
@@ -1226,7 +1225,6 @@
(disc_iffN, disc_iff_thmss, []),
(excludeN, exclude_thmss, []),
(exhaustN, exhaust_thmss, []),
- (nchotomyN, nchotomy_thmss, []),
(selN, sel_thmss, simp_attrs),
(simpsN, simp_thmss, []),
(strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]