# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272456114 -7200
# Node ID 0e2300856d7d5896bb13e5d4731d2ccaf32e4c63
# Parent  14de0767dc7e1fe37744dffbaefca63e3bacf669# Parent  b789c1731fb74ffc46467be65215f4884edb2e6e
merge

diff -r 14de0767dc7e -r 0e2300856d7d src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Apr 28 14:01:13 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Apr 28 14:01:54 2010 +0200
@@ -290,8 +290,7 @@
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
-       Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
-         (*FIXME should not modify base_morph, although admissible*)
+       Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     |> Theory_Target.init (SOME class)
     |> pair class
diff -r 14de0767dc7e -r 0e2300856d7d src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Apr 28 14:01:13 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Apr 28 14:01:54 2010 +0200
@@ -209,6 +209,9 @@
       (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;