diff -r 8a9fd2ffb81d -r bfce186331be src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Jun 09 11:25:21 2021 +0200 +++ b/src/Pure/Isar/class_declaration.ML Wed Jun 09 18:04:21 2021 +0000 @@ -331,10 +331,10 @@ |-> (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, some_axiom, some_assm_intro, of_class) => - Locale.add_registration_theory' + Context.theory_map (Locale.add_registration {inst = (class, base_morph), mixin = Option.map (rpair true) eq_morph, - export = export_morph} + export = export_morph}) #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) |> snd