src/HOL/Tools/datatype_codegen.ML
changeset 22296 c9e7c6e73de3
parent 22175 d9e3e4c30d6b
child 22331 7df6bc8cf0b0
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Sat Feb 10 09:26:14 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Sat Feb 10 09:26:15 2007 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4      -> (string * (((string * sort list) * sort) * term list)) list option
     1.5    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
     1.6      -> (((string * sort list) * sort) list -> (string * term list) list -> theory
     1.7 -    -> ((bstring * attribute list) * term) list * theory)
     1.8 +    -> ((bstring * Attrib.src list) * term) list * theory)
     1.9      -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
    1.10      -> theory -> theory
    1.11