src/HOL/Tools/datatype_package.ML
changeset 18008 f193815cab2c
parent 17956 369e2af8ee45
child 18314 4595eb4627fa
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Oct 28 09:35:04 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 28 09:36:19 2005 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    include BASIC_DATATYPE_PACKAGE
     1.5    val quiet_mode : bool ref
     1.6    val add_datatype : bool -> string list -> (string list * bstring * mixfix *
     1.7 -    (bstring * string list * mixfix) list) list -> theory -> theory *
     1.8 +    (bstring * string list * mixfix) list) list -> theory ->
     1.9        {distinct : thm list list,
    1.10         inject : thm list list,
    1.11         exhaustion : thm list,
    1.12 @@ -27,9 +27,9 @@
    1.13         split_thms : (thm * thm) list,
    1.14         induction : thm,
    1.15         size : thm list,
    1.16 -       simps : thm list}
    1.17 +       simps : thm list} * theory
    1.18    val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
    1.19 -    (bstring * typ list * mixfix) list) list -> theory -> theory *
    1.20 +    (bstring * typ list * mixfix) list) list -> theory ->
    1.21        {distinct : thm list list,
    1.22         inject : thm list list,
    1.23         exhaustion : thm list,
    1.24 @@ -38,10 +38,10 @@
    1.25         split_thms : (thm * thm) list,
    1.26         induction : thm,
    1.27         size : thm list,
    1.28 -       simps : thm list}
    1.29 +       simps : thm list} * theory
    1.30    val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
    1.31      (thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
    1.32 -    theory -> theory *
    1.33 +    theory ->
    1.34        {distinct : thm list list,
    1.35         inject : thm list list,
    1.36         exhaustion : thm list,
    1.37 @@ -50,9 +50,9 @@
    1.38         split_thms : (thm * thm) list,
    1.39         induction : thm,
    1.40         size : thm list,
    1.41 -       simps : thm list}
    1.42 +       simps : thm list} * theory
    1.43    val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
    1.44 -    (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> theory *
    1.45 +    (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory ->
    1.46        {distinct : thm list list,
    1.47         inject : thm list list,
    1.48         exhaustion : thm list,
    1.49 @@ -61,7 +61,7 @@
    1.50         split_thms : (thm * thm) list,
    1.51         induction : thm,
    1.52         size : thm list,
    1.53 -       simps : thm list}
    1.54 +       simps : thm list} * theory
    1.55    val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
    1.56    val print_datatypes : theory -> unit
    1.57    val datatype_info : theory -> string -> DatatypeAux.datatype_info option
    1.58 @@ -377,6 +377,8 @@
    1.59  
    1.60  (**** translation rules for case ****)
    1.61  
    1.62 +fun find_first f = Library.find_first f;
    1.63 +
    1.64  fun case_tr sg [t, u] =
    1.65      let
    1.66        fun case_error s name ts = raise TERM ("Error in case expression" ^
    1.67 @@ -687,8 +689,7 @@
    1.68        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.69        DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    1.70    in
    1.71 -    (thy12,
    1.72 -     {distinct = distinct,
    1.73 +    ({distinct = distinct,
    1.74        inject = inject,
    1.75        exhaustion = exhaustion,
    1.76        rec_thms = rec_thms,
    1.77 @@ -696,7 +697,7 @@
    1.78        split_thms = split_thms,
    1.79        induction = induct,
    1.80        size = size_thms,
    1.81 -      simps = simps})
    1.82 +      simps = simps}, thy12)
    1.83    end;
    1.84  
    1.85  
    1.86 @@ -745,8 +746,7 @@
    1.87        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.88        DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    1.89    in
    1.90 -    (thy12,
    1.91 -     {distinct = distinct,
    1.92 +    ({distinct = distinct,
    1.93        inject = inject,
    1.94        exhaustion = casedist_thms,
    1.95        rec_thms = rec_thms,
    1.96 @@ -754,7 +754,7 @@
    1.97        split_thms = split_thms,
    1.98        induction = induct,
    1.99        size = size_thms,
   1.100 -      simps = simps})
   1.101 +      simps = simps}, thy12)
   1.102    end;
   1.103  
   1.104  
   1.105 @@ -853,8 +853,7 @@
   1.106        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   1.107        DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
   1.108    in
   1.109 -    (thy11,
   1.110 -     {distinct = distinct,
   1.111 +    ({distinct = distinct,
   1.112        inject = inject,
   1.113        exhaustion = casedist_thms,
   1.114        rec_thms = rec_thms,
   1.115 @@ -862,7 +861,7 @@
   1.116        split_thms = split_thms,
   1.117        induction = induction',
   1.118        size = size_thms,
   1.119 -      simps = simps})
   1.120 +      simps = simps}, thy11)
   1.121    end;
   1.122  
   1.123  val rep_datatype = gen_rep_datatype IsarThy.apply_theorems;
   1.124 @@ -968,7 +967,7 @@
   1.125      val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
   1.126      val specs = map (fn ((((_, vs), t), mx), cons) =>
   1.127        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   1.128 -  in #1 o add_datatype false names specs end;
   1.129 +  in snd o add_datatype false names specs end;
   1.130  
   1.131  val datatypeP =
   1.132    OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
   1.133 @@ -981,7 +980,7 @@
   1.134      Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
   1.135      (P.$$$ "induction" |-- P.!!! P.xthm);
   1.136  
   1.137 -fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #1 o rep_datatype opt_ts dss iss ind;
   1.138 +fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
   1.139  
   1.140  val rep_datatypeP =
   1.141    OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl