# HG changeset patch
# User haftmann
# Date 1273042643 -7200
# Node ID bd7f659f7de54ce1cf656d10414e89922bfdd745
# Parent  1342e3aeceeb8d59c0f83e5f4929a78adc308153
tuned interpunctation, dropped dead comment

diff -r 1342e3aeceeb -r bd7f659f7de5 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue May 04 21:04:04 2010 -0700
+++ b/src/Pure/Isar/class.ML	Wed May 05 08:57:23 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Isar/class.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Type classes derived from primitive axclasses and locales - interfaces.
+Type classes derived from primitive axclasses and locales -- interfaces.
 *)
 
 signature CLASS =
diff -r 1342e3aeceeb -r bd7f659f7de5 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Tue May 04 21:04:04 2010 -0700
+++ b/src/Pure/Isar/class_target.ML	Wed May 05 08:57:23 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Isar/class_target.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Type classes derived from primitive axclasses and locales - mechanisms.
+Type classes derived from primitive axclasses and locales -- mechanisms.
 *)
 
 signature CLASS_TARGET =
@@ -209,9 +209,6 @@
       (eq_morph, true) (export_morphism thy cls) thy;
   in fold amend (heritage thy [class]) thy end;
 
-(*fun activate_defs class thms thy = Locale.amend_registration (class, base_morphism thy class)
-  (Element.eq_morphism thy thms, true) (export_morphism thy class) thy;*)
-
 fun register_operation class (c, (t, some_def)) thy =
   let
     val base_sort = base_sort thy class;