src/HOL/Tools/datatype_codegen.ML
changeset 20389 8b6ecb22ef35
parent 20382 39964c8dcd54
child 20426 9ffea7a8b31c
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 16 16:44:41 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Aug 17 09:24:47 2006 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val get_datatype_spec_thms: theory -> string
     1.6      -> (((string * sort) list * (string * typ list) list) * tactic) option
     1.7 -  val get_all_datatype_cons: theory -> (string * string) list
     1.8 +  val datatype_tac: theory -> string -> tactic
     1.9    val dest_case_expr: theory -> term
    1.10      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    1.11    val add_datatype_case_const: string -> theory -> theory
    1.12 @@ -21,7 +21,7 @@
    1.13    val get_datatype_arities: theory -> string list -> sort
    1.14      -> (string * (((string * sort list) * sort) * term list)) list option
    1.15    val prove_arities: (thm list -> tactic) -> string list -> sort
    1.16 -    -> (((string * sort list) * sort) list -> (string * term list) list
    1.17 +    -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
    1.18      -> ((bstring * attribute list) * term) list) -> theory -> theory
    1.19    val setup: theory -> theory
    1.20  end;
    1.21 @@ -392,7 +392,7 @@
    1.22        in
    1.23          thy
    1.24          |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
    1.25 -             arities ("", []) (f arities css)
    1.26 +             arities ("", []) (f thy arities css)
    1.27        end;
    1.28  
    1.29  fun dtyp_of_case_const thy c =
    1.30 @@ -444,12 +444,6 @@
    1.31          SOME (vs_cos, datatype_tac thy dtco)
    1.32      | NONE => NONE;
    1.33  
    1.34 -fun get_all_datatype_cons thy =
    1.35 -  Symtab.fold (fn (dtco, _) => fold
    1.36 -    (fn (co, _) => cons (co, dtco))
    1.37 -      ((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
    1.38 -        (DatatypePackage.get_datatypes thy) [];
    1.39 -
    1.40  fun add_datatype_case_const dtco thy =
    1.41    let
    1.42      val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;