src/HOL/Tools/TFL/tfl.ML
changeset 57983 6edc3529bb4e
parent 56245 84fc7dfa3cd4
child 58111 82db9ad610b9
     1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -434,7 +434,7 @@
     1.4       val case_simpset =
     1.5         put_simpset HOL_basic_ss ctxt
     1.6            addsimps case_rewrites
     1.7 -          |> fold (Simplifier.add_cong o #weak_case_cong o snd)
     1.8 +          |> fold (Simplifier.add_cong o #case_cong_weak o snd)
     1.9                (Symtab.dest (Datatype.get_all theory))
    1.10       val corollaries' = map (Simplifier.simplify case_simpset) corollaries
    1.11       val extract = Rules.CONTEXT_REWRITE_RULE