--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 20:29:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 21:25:53 2013 +0200
@@ -149,8 +149,6 @@
fun s_not @{const True} = @{const False}
| s_not @{const False} = @{const True}
| s_not (@{const Not} $ t) = t
- (* TODO: is the next case really needed? *)
- | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
| s_not t = HOLogic.mk_not t
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};