diff -r 06561afcadaa -r d95a7fd00bd4 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Oct 01 09:09:56 2009 +0200 +++ b/src/Pure/Isar/class.ML Thu Oct 01 17:11:48 2009 +0200 @@ -289,7 +289,7 @@ `(fn thy => calculate thy class sups base_sort param_map assm_axiom) #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) => Locale.add_registration_eqs (class, base_morph) eqs export_morph - #> register class sups params base_sort base_morph axiom assm_intro of_class)) + #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |> TheoryTarget.init (SOME class) |> pair class end;