# HG changeset patch
# User haftmann
# Date 1272454234 -7200
# Node ID 3793f1c83046b066ee0a8dd84477f6f71e870aac
# Parent  70a1e6accac369f515dce7de20dae2dd0e1b44fb
try to observe intended meaning of add_registration interface more closely

diff -r 70a1e6accac3 -r 3793f1c83046 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Apr 28 13:30:17 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Apr 28 13:30:34 2010 +0200
@@ -287,8 +287,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