1.1 --- a/src/Pure/Isar/constdefs.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4      ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
     1.5      theory -> theory
     1.6    val add_constdefs_i: (string * typ option) list *
     1.7 -    ((bstring * typ option * mixfix) option * ((bstring * theory attribute list) * term)) list ->
     1.8 +    ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
     1.9      theory -> theory
    1.10  end;
    1.11  
    1.12 @@ -66,7 +66,7 @@
    1.13    in Pretty.writeln (Specification.pretty_consts ctxt decls); thy' end;
    1.14  
    1.15  val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
    1.16 -  ProofContext.read_term_legacy Attrib.global_attribute;
    1.17 +  ProofContext.read_term_legacy Attrib.attribute;
    1.18  val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
    1.19  
    1.20  end;