Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
1.1 --- a/src/FOL/ex/LocaleTest.thy Thu May 13 13:29:43 2010 +0200
1.2 +++ b/src/FOL/ex/LocaleTest.thy Thu May 13 13:30:16 2010 +0200
1.3 @@ -533,7 +533,7 @@
1.4 grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
1.5 grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
1.6
1.7 -text {* Mixin not applied to locales further up the hierachy. *}
1.8 +text {* Setup *}
1.9
1.10 locale mixin = reflexive
1.11 begin
1.12 @@ -548,16 +548,6 @@
1.13 by (simp add: reflexive.less_def[OF reflexive] gless_def)
1.14 qed
1.15
1.16 -thm le.less_def (* mixin not applied *)
1.17 -lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_def)
1.18 -thm le.less_thm (* mixin applied *)
1.19 -lemma "gless(x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm)
1.20 -
1.21 -lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
1.22 - by (rule le.less_def)
1.23 -lemma "gless(x, y) <-> gle(x, y) & x ~= y"
1.24 - by (rule le.less_thm)
1.25 -
1.26 text {* Mixin propagated along the locale hierarchy *}
1.27
1.28 locale mixin2 = mixin
2.1 --- a/src/Pure/Isar/locale.ML Thu May 13 13:29:43 2010 +0200
2.2 +++ b/src/Pure/Isar/locale.ML Thu May 13 13:30:16 2010 +0200
2.3 @@ -384,9 +384,10 @@
2.4 |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
2.5 (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
2.6
2.7 -fun all_registrations thy = Registrations.get thy
2.8 - |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
2.9 - (* without inherited mixins *)
2.10 +fun all_registrations thy = Registrations.get thy (* FIXME clone *)
2.11 + (* with inherited mixins *)
2.12 + |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
2.13 + (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
2.14
2.15 fun activate_notes' activ_elem transfer thy export (name, morph) input =
2.16 let
2.17 @@ -462,19 +463,21 @@
2.18 fun add_registration (name, base_morph) mixin export thy =
2.19 let
2.20 val base = instance_of thy name base_morph;
2.21 + val mix = case mixin of NONE => Morphism.identity
2.22 + | SOME (mix, _) => mix;
2.23 in
2.24 if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
2.25 then thy
2.26 else
2.27 (get_idents (Context.Theory thy), thy)
2.28 (* add new registrations with inherited mixins *)
2.29 - |> roundup thy (add_reg export) export (name, base_morph)
2.30 + |> roundup thy (add_reg export) export (name, base_morph $> mix) (* FIXME *)
2.31 |> snd
2.32 (* add mixin *)
2.33 |> (case mixin of NONE => I
2.34 - | SOME mixin => amend_registration (name, base_morph) mixin export)
2.35 + | SOME mixin => amend_registration (name, base_morph $> mix) mixin export)
2.36 (* activate import hierarchy as far as not already active *)
2.37 - |> Context.theory_map (activate_facts' export (name, base_morph))
2.38 + |> Context.theory_map (activate_facts' export (name, base_morph $> mix))
2.39 end;
2.40
2.41