1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Jun 23 15:32:34 2009 +0200
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Jun 23 16:27:12 2009 +0200
     1.3 @@ -446,7 +446,7 @@
     1.4         slow.*)
     1.5       val case_ss = Simplifier.theory_context theory
     1.6         (HOL_basic_ss addcongs
     1.7 -         (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) theory addsimps case_rewrites)
     1.8 +         (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
     1.9       val corollaries' = map (Simplifier.simplify case_ss) corollaries
    1.10       val extract = R.CONTEXT_REWRITE_RULE
    1.11                       (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)