1.1 --- a/src/Pure/Isar/class.ML	Tue May 04 21:04:04 2010 -0700
     1.2 +++ b/src/Pure/Isar/class.ML	Wed May 05 08:57:23 2010 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/Isar/class.ML
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Type classes derived from primitive axclasses and locales - interfaces.
     1.8 +Type classes derived from primitive axclasses and locales -- interfaces.
     1.9  *)
    1.10  
    1.11  signature CLASS =

     2.1 --- a/src/Pure/Isar/class_target.ML	Tue May 04 21:04:04 2010 -0700
     2.2 +++ b/src/Pure/Isar/class_target.ML	Wed May 05 08:57:23 2010 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      Pure/Isar/class_target.ML
     2.5      Author:     Florian Haftmann, TU Muenchen
     2.6  
     2.7 -Type classes derived from primitive axclasses and locales - mechanisms.
     2.8 +Type classes derived from primitive axclasses and locales -- mechanisms.
     2.9  *)
    2.10  
    2.11  signature CLASS_TARGET =
    2.12 @@ -209,9 +209,6 @@
    2.13        (eq_morph, true) (export_morphism thy cls) thy;
    2.14    in fold amend (heritage thy [class]) thy end;
    2.15  
    2.16 -(*fun activate_defs class thms thy = Locale.amend_registration (class, base_morphism thy class)
    2.17 -  (Element.eq_morphism thy thms, true) (export_morphism thy class) thy;*)
    2.18 -
    2.19  fun register_operation class (c, (t, some_def)) thy =
    2.20    let
    2.21      val base_sort = base_sort thy class;