src/HOL/HOL.thy
changeset 52230 1105b3b5aa77
parent 52143 36ffe23b25f8
child 52432 c03090937c3b
     1.1 --- a/src/HOL/HOL.thy	Thu May 30 08:27:51 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu May 30 12:35:40 2013 +0200
     1.3 @@ -1499,8 +1499,7 @@
     1.4                  in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
     1.5                | _ => NONE))]
     1.6      |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
     1.7 -      map (Simplifier.rewrite_rule (map Thm.symmetric
     1.8 -        @{thms induct_rulify_fallback})))))
     1.9 +      map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
    1.10  *}
    1.11  
    1.12  text {* Pre-simplification of induction and cases rules *}