--- a/src/Pure/axclass.ML Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/axclass.ML Sun Feb 07 19:33:34 2010 +0100
@@ -484,10 +484,10 @@
def_thy
|> Sign.mandatory_path (Binding.name_of bconst)
|> PureThy.note_thmss ""
- [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
- ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
+ [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
+ ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
((Binding.name axiomsN, []),
- [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
+ [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
||> Sign.restore_naming def_thy;