src/HOL/HOL.thy
changeset 45625 750c5a47400b
parent 45607 16b4f5774621
child 45654 cf10bde35973
     1.1 --- a/src/HOL/HOL.thy	Thu Nov 24 20:45:34 2011 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Nov 24 21:01:06 2011 +0100
     1.3 @@ -1495,9 +1495,6 @@
     1.4  setup {*
     1.5    Induct.setup #> Induction.setup #>
     1.6    Context.theory_map (Induct.map_simpset (fn ss => ss
     1.7 -    setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
     1.8 -      map (Simplifier.rewrite_rule (map Thm.symmetric
     1.9 -        @{thms induct_rulify_fallback})))
    1.10      addsimprocs
    1.11        [Simplifier.simproc_global @{theory} "swap_induct_false"
    1.12           ["induct_false ==> PROP P ==> PROP Q"]
    1.13 @@ -1517,7 +1514,10 @@
    1.14                      | is_conj @{const induct_false} = true
    1.15                      | is_conj _ = false
    1.16                  in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
    1.17 -              | _ => NONE))]))
    1.18 +              | _ => NONE))]
    1.19 +    |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
    1.20 +      map (Simplifier.rewrite_rule (map Thm.symmetric
    1.21 +        @{thms induct_rulify_fallback})))))
    1.22  *}
    1.23  
    1.24  text {* Pre-simplification of induction and cases rules *}