src/HOL/HOL.thy
changeset 62913 13252110a6fe
parent 62522 d32c23d29968
child 62958 b41c1cb5e251
     1.1 --- a/src/HOL/HOL.thy	Thu Apr 07 22:09:23 2016 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 08 20:15:20 2016 +0200
     1.3 @@ -1444,8 +1444,7 @@
     1.4            (case Thm.term_of ct of
     1.5              _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
     1.6                if P <> Q then SOME Drule.swap_prems_eq else NONE
     1.7 -          | _ => NONE),
     1.8 -         identifier = []},
     1.9 +          | _ => NONE)},
    1.10         Simplifier.make_simproc @{context} "induct_equal_conj_curry"
    1.11          {lhss = [@{term "induct_conj P Q \<Longrightarrow> PROP R"}],
    1.12           proc = fn _ => fn _ => fn ct =>
    1.13 @@ -1459,8 +1458,7 @@
    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 -          identifier = []}]
    1.19 +            | _ => NONE)}]
    1.20      |> Simplifier.set_mksimps (fn ctxt =>
    1.21          Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
    1.22          map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
    1.23 @@ -1759,8 +1757,7 @@
    1.24           proc = fn _ => fn _ => fn ct =>
    1.25            (case Thm.term_of ct of
    1.26              Const (_, Type (@{type_name fun}, [Type _, _])) => SOME @{thm eq_equal}
    1.27 -          | _ => NONE),
    1.28 -         identifier = []}])
    1.29 +          | _ => NONE)}])
    1.30  \<close>
    1.31  
    1.32