src/HOL/Tools/datatype_codegen.ML
changeset 22331 7df6bc8cf0b0
parent 22296 c9e7c6e73de3
child 22423 c1836b14c63a
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Feb 16 19:19:19 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Feb 16 22:13:15 2007 +0100
     1.3 @@ -25,11 +25,11 @@
     1.4    val the_codetypes_mut_specs: theory -> (string * bool) list
     1.5      -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
     1.6    val get_codetypes_arities: theory -> (string * bool) list -> sort
     1.7 -    -> (string * (((string * sort list) * sort) * term list)) list option
     1.8 +    -> (string * (arity * term list)) list option
     1.9    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
    1.10 -    -> (((string * sort list) * sort) list -> (string * term list) list -> theory
    1.11 +    -> (arity list -> (string * term list) list -> theory
    1.12      -> ((bstring * Attrib.src list) * term) list * theory)
    1.13 -    -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
    1.14 +    -> (arity list -> (string * term list) list -> theory -> theory)
    1.15      -> theory -> theory
    1.16  
    1.17    val setup: theory -> theory
    1.18 @@ -584,11 +584,10 @@
    1.19            (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
    1.20        in (c, tys') end;
    1.21      val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto;
    1.22 -    fun mk_arity tyco =
    1.23 -      ((tyco, map snd vs), sort);
    1.24 +    fun mk_arity tyco = (tyco, map snd vs, sort);
    1.25      fun typ_of_sort ty =
    1.26        let
    1.27 -        val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
    1.28 +        val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css;
    1.29        in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
    1.30      fun mk_cons tyco (c, tys) =
    1.31        let
    1.32 @@ -605,7 +604,7 @@
    1.33    case get_codetypes_arities thy tycos sort
    1.34     of NONE => thy
    1.35      | SOME insts => let
    1.36 -        fun proven ((tyco, asorts), sort) =
    1.37 +        fun proven (tyco, asorts, sort) =
    1.38            Sorts.of_sort (Sign.classes_of thy)
    1.39              (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
    1.40          val (arities, css) = (split_list o map_filter