--- a/src/Pure/Isar/constdefs.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/constdefs.ML Sat Jan 21 23:02:14 2006 +0100
@@ -13,7 +13,7 @@
((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
theory -> theory
val add_constdefs_i: (string * typ option) list *
- ((bstring * typ option * mixfix) option * ((bstring * theory attribute list) * term)) list ->
+ ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
theory -> theory
end;
@@ -66,7 +66,7 @@
in Pretty.writeln (Specification.pretty_consts ctxt decls); thy' end;
val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
- ProofContext.read_term_legacy Attrib.global_attribute;
+ ProofContext.read_term_legacy Attrib.attribute;
val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
end;