src/HOL/Tools/datatype_codegen.ML
changeset 24423 ae9cd0e92423
parent 24219 e558fe311376
child 24428 fcf429a4e923
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
     1.5      -> (arity list -> (string * term list) list -> theory
     1.6        -> ((bstring * Attrib.src list) * term) list * theory)
     1.7 -    -> (arity list -> (string * term list) list -> theory -> theory)
     1.8 +    -> (arity list -> (string * term list) list -> thm list -> theory -> theory)
     1.9      -> theory -> theory
    1.10  
    1.11    val setup: theory -> theory
    1.12 @@ -537,8 +537,13 @@
    1.13  
    1.14  (* registering code types in code generator *)
    1.15  
    1.16 -fun codetype_hook dtspecs =
    1.17 -  fold (fn (dtco, (_, spec)) => Code.add_datatype (dtco, spec)) dtspecs;
    1.18 +fun add_datatype_spec (tyco, (vs, cos)) thy =
    1.19 +  let
    1.20 +    val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
    1.21 +  in try (Code.add_datatype cs) thy |> the_default thy end;
    1.22 +
    1.23 +val codetype_hook =
    1.24 +  fold (fn (dtco, (_, spec)) => add_datatype_spec (dtco, spec));
    1.25  
    1.26  
    1.27  (* instrumentalizing the sort algebra *)
    1.28 @@ -586,7 +591,8 @@
    1.29              f arities css
    1.30              #-> (fn defs =>
    1.31                Class.prove_instance_arity tac arities defs
    1.32 -            #> after_qed arities css))
    1.33 +            #-> (fn defs =>
    1.34 +              after_qed arities css defs)))
    1.35        end;
    1.36  
    1.37  
    1.38 @@ -597,7 +603,7 @@
    1.39      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
    1.40        let
    1.41          val thy_ref = Theory.check_thy thy;
    1.42 -        val const = ("op =", SOME dtco);
    1.43 +        val const = Class.inst_const thy ("op =", dtco);
    1.44          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    1.45        in
    1.46          Code.add_funcl (const, Susp.delay get_thms) thy
    1.47 @@ -605,7 +611,7 @@
    1.48    in
    1.49      prove_codetypes_arities (Class.intro_classes_tac [])
    1.50        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    1.51 -      [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
    1.52 +      [HOLogic.class_eq] ((K o K o pair) []) ((K o K o K) (fold add_eq_thms specs))
    1.53    end;
    1.54  
    1.55