src/HOL/Tools/Datatype/datatype.ML
changeset 31783 cfbe9609ceb1
parent 31781 861e675f01e6
child 31784 bd3486c57ba3
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 14:51:21 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 15:32:34 2009 +0200
     1.3 @@ -8,11 +8,7 @@
     1.4  sig
     1.5    include DATATYPE_COMMON
     1.6    val add_datatype : config -> string list -> (string list * binding * mixfix *
     1.7 -    (binding * typ list * mixfix) list) list -> theory ->
     1.8 -     (string list * {inject : thm list list,
     1.9 -      rec_thms : thm list,
    1.10 -      case_thms : thm list list,
    1.11 -      induction : thm}) * theory
    1.12 +    (binding * typ list * mixfix) list) list -> theory -> string list * theory
    1.13    val datatype_cmd : string list -> (string list * binding * mixfix *
    1.14      (binding * string list * mixfix) list) list -> theory -> theory
    1.15    val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    1.16 @@ -381,12 +377,7 @@
    1.17        |> Sign.parent_path
    1.18        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.19        |> DatatypeInterpretation.data (config, map fst dt_infos);
    1.20 -  in
    1.21 -    ((dt_names, {inject = inject,
    1.22 -      rec_thms = rec_thms,
    1.23 -      case_thms = case_thms,
    1.24 -      induction = induct}), thy12)
    1.25 -  end;
    1.26 +  in (dt_names, thy12) end;
    1.27  
    1.28  
    1.29  (*********************** declare existing type as datatype *********************)