src/Pure/Isar/class.ML
changeset 38107 3a46cebd7983
parent 37101 7099a9ed3be2
child 38350 480b2de9927c
--- a/src/Pure/Isar/class.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/Pure/Isar/class.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -293,8 +293,8 @@
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
-       Locale.add_registration (class, base_morph)
-         (Option.map (rpair true) eq_morph) export_morph
+       Context.theory_map (Locale.add_registration (class, base_morph)
+         (Option.map (rpair true) eq_morph) export_morph)
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     |> Theory_Target.init (SOME class)
     |> pair class