diff -r 68496cc300a4 -r 53943f4dab21 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Sat Apr 14 17:36:18 2007 +0200 +++ b/src/Pure/Tools/codegen_package.ML Sat Apr 14 17:36:19 2007 +0200 @@ -547,7 +547,7 @@ in val abstyp = gen_abstyp (K I) Sign.certify_typ; -val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE)); +val abstyp_e = gen_abstyp CodegenConsts.read_const Sign.read_typ; val constsubst = gen_constsubst (K I); val constsubst_e = gen_constsubst CodegenConsts.read_const; @@ -606,7 +606,6 @@ fun consts_of thy thyname = let val this_thy = Option.map theory thyname |> the_default thy; - val defs = (#defs o rep_theory) thy; val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) []; fun classop c = case AxClass.class_of_param thy c