--- 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 =
--- 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;