# HG changeset patch
# User ballarin
# Date 1273865009 -7200
# Node ID 182774d56bd2279909dba0ada750c36cc313a782
# Parent  e65f8d253fd15dd9ca4522d9312d48760436dbf1
Revert mixin patch due to inacceptable performance drop.

diff -r e65f8d253fd1 -r 182774d56bd2 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Fri May 14 15:27:07 2010 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Fri May 14 21:23:29 2010 +0200
@@ -533,7 +533,7 @@
   grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
   grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
 
-text {* Setup *}
+text {* Mixin not applied to locales further up the hierachy. *}
 
 locale mixin = reflexive
 begin
@@ -548,6 +548,16 @@
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
+thm le.less_def  (* mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_def)
+thm le.less_thm  (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm)
+
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+  by (rule le.less_def)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le.less_thm)
+
 text {* Mixin propagated along the locale hierarchy *}
 
 locale mixin2 = mixin
diff -r e65f8d253fd1 -r 182774d56bd2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri May 14 15:27:07 2010 +0200
+++ b/src/Pure/Isar/class.ML	Fri May 14 21:23:29 2010 +0200
@@ -293,7 +293,8 @@
     |-> (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)
+       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*)
          (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)
diff -r e65f8d253fd1 -r 182774d56bd2 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri May 14 15:27:07 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Fri May 14 21:23:29 2010 +0200
@@ -384,10 +384,9 @@
   |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
     (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
 
-fun all_registrations thy = Registrations.get thy (* FIXME clone *)
-  (* with inherited mixins *)
-  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
-    (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
+fun all_registrations thy = Registrations.get thy
+  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
+  (* without inherited mixins *)
 
 fun activate_notes' activ_elem transfer thy export (name, morph) input =
   let
@@ -463,21 +462,19 @@
 fun add_registration (name, base_morph) mixin export thy =
   let
     val base = instance_of thy name base_morph;
-    val mix = case mixin of NONE => Morphism.identity
-          | SOME (mix, _) => mix;
   in
     if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
     then thy
     else
       (get_idents (Context.Theory thy), thy)
       (* add new registrations with inherited mixins *)
-      |> roundup thy (add_reg export) export (name, base_morph $> mix) (* FIXME *)
+      |> roundup thy (add_reg export) export (name, base_morph)
       |> snd
       (* add mixin *)
       |> (case mixin of NONE => I
-           | SOME mixin => amend_registration (name, base_morph $> mix) mixin export)
+           | SOME mixin => amend_registration (name, base_morph) mixin export)
       (* activate import hierarchy as far as not already active *)
-      |> Context.theory_map (activate_facts' export (name, base_morph $> mix))
+      |> Context.theory_map (activate_facts' export (name, base_morph))
   end;