# HG changeset patch
# User haftmann
# Date 1281614022 -7200
# Node ID 8a3ca8b96b23270dd072bc1c5e1ca4e55cc6cdd1
# Parent  ba1cc1815ce1b7f8e77a8c977000a2226835a015
Class.declare -> Class.const

diff -r ba1cc1815ce1 -r 8a3ca8b96b23 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Aug 12 13:42:13 2010 +0200
+++ b/src/Pure/Isar/class.ML	Thu Aug 12 13:53:42 2010 +0200
@@ -17,7 +17,7 @@
   val print_classes: theory -> unit
   val init: class -> theory -> Proof.context
   val begin: class list -> sort -> Proof.context -> Proof.context
-  val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
+  val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory
   val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
   val refresh_syntax: class -> Proof.context -> Proof.context
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
@@ -312,7 +312,7 @@
 
 val class_prefix = Logic.const_of_class o Long_Name.base_name;
 
-fun declare class ((c, mx), (type_params, dict)) thy =
+fun const class ((c, mx), (type_params, dict)) thy =
   let
     val morph = morphism thy class;
     val b = Morphism.binding morph c;
diff -r ba1cc1815ce1 -r 8a3ca8b96b23 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Aug 12 13:42:13 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:53:42 2010 +0200
@@ -104,7 +104,7 @@
     (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
-    #> class_target ta (Class.declare target ((b, mx), (type_params, lhs)))
+    #> class_target ta (Class.const target ((b, mx), (type_params, lhs)))
     #> pair (lhs, def))
 
 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =