src/Pure/Isar/class.ML
changeset 38392 8a3ca8b96b23
parent 38384 07c33be08476
child 38619 25e401d53900
     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;