src/Pure/Isar/class.ML
changeset 36919 182774d56bd2
parent 36904 3e200347a22e
child 37101 7099a9ed3be2
     1.1 --- a/src/Pure/Isar/class.ML	Fri May 14 15:27:07 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri May 14 21:23:29 2010 +0200
     1.3 @@ -293,7 +293,8 @@
     1.4      |-> (fn (param_map, params, assm_axiom) =>
     1.5         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     1.6      #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
     1.7 -       Locale.add_registration (class, base_morph)
     1.8 +       Locale.add_registration (class, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph)
     1.9 +         (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*)
    1.10           (Option.map (rpair true) eq_morph) export_morph
    1.11      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.12      |> Theory_Target.init (SOME class)