Fixed inefficiency in post_definition by adding weak case congruence
rules to simpset.
--- a/TFL/tfl.ML Tue Sep 30 17:05:50 2003 +0200
+++ b/TFL/tfl.ML Wed Oct 01 11:02:36 2003 +0200
@@ -446,7 +446,9 @@
val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
given_pats
val (case_rewrites,context_congs) = extraction_thms theory
- val corollaries' = map(rewrite_rule case_rewrites) corollaries
+ val case_ss = HOL_basic_ss addcongs
+ DatatypePackage.weak_case_congs_of theory addsimps case_rewrites
+ val corollaries' = map (Simplifier.simplify case_ss) corollaries
val extract = R.CONTEXT_REWRITE_RULE
(f, [R], cut_apply, meta_tflCongs@context_congs)
val (rules, TCs) = ListPair.unzip (map extract corollaries')