src/Pure/Isar/class.ML
changeset 36464 b789c1731fb7
parent 36460 c643b23e8592
parent 36463 3793f1c83046
child 36610 bafd82950e24
child 36635 080b755377c0
     1.1 --- a/src/Pure/Isar/class.ML	Wed Apr 28 13:29:57 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Apr 28 13:30:52 2010 +0200
     1.3 @@ -290,8 +290,7 @@
     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 $> eq_morph) NONE export_morph
     1.8 -         (*FIXME should not modify base_morph, although admissible*)
     1.9 +       Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph
    1.10      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.11      |> Theory_Target.init (SOME class)
    1.12      |> pair class