src/HOL/Tools/datatype_codegen.ML
changeset 21924 fe474e69e603
parent 21708 45e7491bea47
child 22047 ff91fd74bb71
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 29 03:57:01 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 29 12:11:00 2006 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4      -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
     1.5    val get_codetypes_arities: theory -> (string * bool) list -> sort
     1.6      -> (string * (((string * sort list) * sort) * term list)) list option
     1.7 -  val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
     1.8 +  val prove_codetypes_arities: tactic -> (string * bool) list -> sort
     1.9      -> (((string * sort list) * sort) list -> (string * term list) list -> theory
    1.10      -> ((bstring * attribute list) * term) list * theory)
    1.11      -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
    1.12 @@ -612,7 +612,7 @@
    1.13          |> not (null arities) ? (
    1.14              f arities css
    1.15              #-> (fn defs =>
    1.16 -              ClassPackage.prove_instance_arity tac arities ("", []) defs
    1.17 +              ClassPackage.prove_instance_arity tac arities defs
    1.18              #> after_qed arities css))
    1.19        end;
    1.20  
    1.21 @@ -631,7 +631,7 @@
    1.22          CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
    1.23        end;
    1.24    in
    1.25 -    prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
    1.26 +    prove_codetypes_arities (ClassPackage.intro_classes_tac [])
    1.27        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    1.28        [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
    1.29    end;