1.1 --- a/src/Pure/Isar/class_target.ML	Thu Oct 01 09:09:56 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Thu Oct 01 17:11:48 2009 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    (*classes*)
     1.6    val register: class -> class list -> ((string * typ) * (string * typ)) list
     1.7 -    -> sort -> morphism -> thm option -> thm option -> thm
     1.8 +    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
     1.9      -> theory -> theory
    1.10  
    1.11    val is_class: theory -> class -> bool
    1.12 @@ -78,6 +78,7 @@
    1.13    base_sort: sort,
    1.14    base_morph: morphism
    1.15      (*static part of canonical morphism*),
    1.16 +  export_morph: morphism,
    1.17    assm_intro: thm option,
    1.18    of_class: thm,
    1.19    axiom: thm option,
    1.20 @@ -88,21 +89,21 @@
    1.21  
    1.22  };
    1.23  
    1.24 -fun make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.25 +fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    1.26      (defs, operations)) =
    1.27    ClassData { consts = consts, base_sort = base_sort,
    1.28 -    base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    1.29 -    defs = defs, operations = operations };
    1.30 -fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
    1.31 +    base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
    1.32 +    of_class = of_class, axiom = axiom, defs = defs, operations = operations };
    1.33 +fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
    1.34      of_class, axiom, defs, operations }) =
    1.35 -  make_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.36 +  make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    1.37      (defs, operations)));
    1.38  fun merge_class_data _ (ClassData { consts = consts,
    1.39 -    base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
    1.40 +    base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
    1.41      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    1.42 -  ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
    1.43 +  ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
    1.44      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    1.45 -  make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.46 +  make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    1.47      (Thm.merge_thms (defs1, defs2),
    1.48        AList.merge (op =) (K true) (operations1, operations2)));
    1.49  
    1.50 @@ -159,6 +160,7 @@
    1.51  val base_morphism = #base_morph oo the_class_data;
    1.52  fun morphism thy class = base_morphism thy class
    1.53    $> Element.eq_morphism thy (these_defs thy [class]);
    1.54 +val export_morphism = #export_morph oo the_class_data;
    1.55  
    1.56  fun print_classes thy =
    1.57    let
    1.58 @@ -196,22 +198,22 @@
    1.59  
    1.60  (* updaters *)
    1.61  
    1.62 -fun register class sups params base_sort morph
    1.63 +fun register class sups params base_sort base_morph export_morph
    1.64      axiom assm_intro of_class thy =
    1.65    let
    1.66      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    1.67        (c, (class, (ty, Free v_ty)))) params;
    1.68      val add_class = Graph.new_node (class,
    1.69          make_class_data (((map o pairself) fst params, base_sort,
    1.70 -          morph, assm_intro, of_class, axiom), ([], operations)))
    1.71 +          base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
    1.72        #> fold (curry Graph.add_edge class) sups;
    1.73    in ClassData.map add_class thy end;
    1.74  
    1.75  fun activate_defs class thms thy =
    1.76    let
    1.77      val eq_morph = Element.eq_morphism thy thms;
    1.78 -    fun amend cls thy = Locale.amend_registration_legacy eq_morph
    1.79 -      (cls, morphism thy cls) thy;
    1.80 +    fun amend cls thy = Locale.amend_registration (cls, base_morphism thy cls)
    1.81 +      (eq_morph, true) (export_morphism thy cls) thy;
    1.82    in fold amend (heritage thy [class]) thy end;
    1.83  
    1.84  fun register_operation class (c, (t, some_def)) thy =