dropped induction rule
authorhaftmann
Tue Dec 11 10:23:11 2007 +0100 (2007-12-11 ago)
changeset 256046c1714b9b805
parent 25603 4b7a58fc168c
child 25605 35a5f7f4b97b
dropped induction rule
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Dec 11 10:23:10 2007 +0100
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Dec 11 10:23:11 2007 +0100
     1.3 @@ -204,20 +204,6 @@
     1.4              else find_dts dt_info tnames' tnames);
     1.5  
     1.6  
     1.7 -(* adapted induction rule *)
     1.8 -
     1.9 -fun prepare_induct ({descr, induction, ...}: datatype_info) eqns =
    1.10 -  let
    1.11 -    fun constrs_of (_, (_, _, cs)) =
    1.12 -      map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
    1.13 -    val params_of = these o AList.lookup (op =) (List.concat (map constrs_of eqns));
    1.14 -  in
    1.15 -    induction
    1.16 -    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
    1.17 -    |> RuleCases.save induction
    1.18 -  end;
    1.19 -
    1.20 -
    1.21  (* primrec definition *)
    1.22  
    1.23  local
    1.24 @@ -267,9 +253,7 @@
    1.25      |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
    1.26      |-> (fn simps' => LocalTheory.note Thm.theoremK
    1.27            ((qualify "simps", simp_atts), maps snd simps'))
    1.28 -    ||>> LocalTheory.note Thm.theoremK
    1.29 -          ((qualify "induct", []), [prepare_induct (#2 (hd dts)) eqns])
    1.30 -    |>> (snd o fst)
    1.31 +    |>> snd
    1.32    end handle PrimrecError (msg, some_eqn) =>
    1.33      error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
    1.34       of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)