src/HOL/HOL.thy
changeset 54742 7a86358a3c0b
parent 53146 3a93bc5d3370
child 54890 cb892d835803
     1.1 --- a/src/HOL/HOL.thy	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -1496,8 +1496,9 @@
     1.4                      | is_conj _ = false
     1.5                  in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
     1.6                | _ => NONE))]
     1.7 -    |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
     1.8 -      map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
     1.9 +    |> Simplifier.set_mksimps (fn ctxt =>
    1.10 +        Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
    1.11 +        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
    1.12  *}
    1.13  
    1.14  text {* Pre-simplification of induction and cases rules *}