src/HOL/Library/Eval.thy
changeset 24423 ae9cd0e92423
parent 24381 560e8ecdf633
child 24508 c8b82fec6447
     1.1 --- a/src/HOL/Library/Eval.thy	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    fun hook specs =
     1.5      DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
     1.6        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
     1.7 -      [TypOf.class_typ_of] mk ((K o K) I)
     1.8 +      [TypOf.class_typ_of] mk ((K o K) (fold (Code.add_func true)))
     1.9  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    1.10  *}
    1.11  
    1.12 @@ -98,7 +98,7 @@
    1.13      PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
    1.14    fun thy_def ((name, atts), t) =
    1.15      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
    1.16 -  fun mk arities css thy =
    1.17 +  fun mk arities css _ thy =
    1.18      let
    1.19        val (_, asorts, _) :: _ = arities;
    1.20        val vs = Name.names Name.context "'a" asorts;