src/Pure/Isar/constdefs.ML

--- 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;