--- a/TFL/tfl.ML Thu Oct 02 10:57:04 2003 +0200
+++ b/TFL/tfl.ML Fri Oct 03 12:36:16 2003 +0200
@@ -446,6 +446,9 @@
val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
given_pats
val (case_rewrites,context_congs) = extraction_thms theory
+ (*case_ss causes minimal simplification: bodies of case expressions are
+ not simplified. Otherwise large examples (Red-Black trees) are too
+ slow.*)
val case_ss = HOL_basic_ss addcongs
DatatypePackage.weak_case_congs_of theory addsimps case_rewrites
val corollaries' = map (Simplifier.simplify case_ss) corollaries