# HG changeset patch
# User berghofe
# Date 1064998956 -7200
# Node ID 9f5679e97eac2e1da74b726e05766f8d43440cea
# Parent  a15951091d5d3688216ff987da7f43fce4dacf53
Fixed inefficiency in post_definition by adding weak case congruence
rules to simpset.

diff -r a15951091d5d -r 9f5679e97eac TFL/tfl.ML
--- 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')