# HG changeset patch
# User ballarin
# Date 1273750183 -7200
# Node ID 3e200347a22e53199bc1e947755e90bc1b94a9c4
# Parent  c6bae4456741758122c0bf2e2c85fb57167324da
Remove improper use of mixin in class package.

diff -r c6bae4456741 -r 3e200347a22e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed May 12 22:33:10 2010 -0700
+++ b/src/Pure/Isar/class.ML	Thu May 13 13:29:43 2010 +0200
@@ -293,8 +293,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, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph)
-         (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*)
+       Locale.add_registration (class, base_morph)
          (Option.map (rpair true) eq_morph) export_morph
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     |> Theory_Target.init (SOME class)