merged

--- a/src/HOL/Relation.thy	Fri Oct 02 00:10:08 2009 +0200
+++ b/src/HOL/Relation.thy	Fri Oct 02 04:44:56 2009 +0200
@@ -6,8 +6,7 @@
 header {* Relations *}
 
 theory Relation
-imports Finite_Set Datatype
-  (*FIXME order is important, otherwise merge problem for canonical interpretation of class monoid_mult wrt. power!*)
+imports Datatype Finite_Set
 begin
 
 subsection {* Definitions *}

--- a/src/Pure/Isar/class.ML	Fri Oct 02 00:10:08 2009 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 02 04:44:56 2009 +0200
@@ -289,7 +289,7 @@
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
        Locale.add_registration_eqs (class, base_morph) eqs export_morph
-    #> register class sups params base_sort base_morph axiom assm_intro of_class))
+    #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     |> TheoryTarget.init (SOME class)
     |> pair class
   end;

--- a/src/Pure/Isar/class_target.ML	Fri Oct 02 00:10:08 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Fri Oct 02 04:44:56 2009 +0200
@@ -8,7 +8,7 @@
 sig
   (*classes*)
   val register: class -> class list -> ((string * typ) * (string * typ)) list
-    -> sort -> morphism -> thm option -> thm option -> thm
+    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
     -> theory -> theory
 
   val is_class: theory -> class -> bool
@@ -78,6 +78,7 @@
   base_sort: sort,
   base_morph: morphism
     (*static part of canonical morphism*),
+  export_morph: morphism,
   assm_intro: thm option,
   of_class: thm,
   axiom: thm option,
@@ -88,21 +89,21 @@
 
 };
 
-fun make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
+fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)) =
   ClassData { consts = consts, base_sort = base_sort,
-    base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
-    defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
+    base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
+    of_class = of_class, axiom = axiom, defs = defs, operations = operations };
+fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
     of_class, axiom, defs, operations }) =
-  make_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
+  make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)));
 fun merge_class_data _ (ClassData { consts = consts,
-    base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
+    base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
-  ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
+  ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
     of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
-  make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
+  make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (Thm.merge_thms (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
@@ -159,6 +160,7 @@
 val base_morphism = #base_morph oo the_class_data;
 fun morphism thy class = base_morphism thy class
   $> Element.eq_morphism thy (these_defs thy [class]);
+val export_morphism = #export_morph oo the_class_data;
 
 fun print_classes thy =
   let
@@ -196,22 +198,22 @@
 
 (* updaters *)
 
-fun register class sups params base_sort morph
+fun register class sups params base_sort base_morph export_morph
     axiom assm_intro of_class thy =
   let
     val operations = map (fn (v_ty as (_, ty), (c, _)) =>
       (c, (class, (ty, Free v_ty)))) params;
     val add_class = Graph.new_node (class,
         make_class_data (((map o pairself) fst params, base_sort,
-          morph, assm_intro, of_class, axiom), ([], operations)))
+          base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
       #> fold (curry Graph.add_edge class) sups;
   in ClassData.map add_class thy end;
 
 fun activate_defs class thms thy =
   let
     val eq_morph = Element.eq_morphism thy thms;
-    fun amend cls thy = Locale.amend_registration_legacy eq_morph
-      (cls, morphism thy cls) thy;
+    fun amend cls thy = Locale.amend_registration (cls, base_morphism thy cls)
+      (eq_morph, true) (export_morphism thy cls) thy;
   in fold amend (heritage thy [class]) thy end;
 
 fun register_operation class (c, (t, some_def)) thy =