1.1 --- a/src/Pure/Isar/class.ML	Thu Aug 12 13:42:13 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Aug 12 13:53:42 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val print_classes: theory -> unit
     1.5    val init: class -> theory -> Proof.context
     1.6    val begin: class list -> sort -> Proof.context -> Proof.context
     1.7 -  val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
     1.8 +  val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory
     1.9    val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
    1.10    val refresh_syntax: class -> Proof.context -> Proof.context
    1.11    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.12 @@ -312,7 +312,7 @@
    1.13  
    1.14  val class_prefix = Logic.const_of_class o Long_Name.base_name;
    1.15  
    1.16 -fun declare class ((c, mx), (type_params, dict)) thy =
    1.17 +fun const class ((c, mx), (type_params, dict)) thy =
    1.18    let
    1.19      val morph = morphism thy class;
    1.20      val b = Morphism.binding morph c;

     2.1 --- a/src/Pure/Isar/named_target.ML	Thu Aug 12 13:42:13 2010 +0200
     2.2 +++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:53:42 2010 +0200
     2.3 @@ -104,7 +104,7 @@
     2.4      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
     2.5    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
     2.6    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
     2.7 -    #> class_target ta (Class.declare target ((b, mx), (type_params, lhs)))
     2.8 +    #> class_target ta (Class.const target ((b, mx), (type_params, lhs)))
     2.9      #> pair (lhs, def))
    2.10  
    2.11  fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =