--- a/src/Pure/Isar/class_declaration.ML Thu Aug 30 12:36:26 2018 +0200
+++ b/src/Pure/Isar/class_declaration.ML Thu Aug 30 13:38:52 2018 +0200
@@ -328,8 +328,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) =>
- Context.theory_map (Locale.add_registration (class, base_morph)
- (Option.map (rpair true) eq_morph) export_morph)
+ Context.theory_map (Locale.add_registration
+ {dep = (class, base_morph),
+ mixin = Option.map (rpair true) eq_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