--- a/src/Pure/Isar/class.ML Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/class.ML Sun Feb 07 19:33:34 2010 +0100
@@ -86,7 +86,7 @@
| SOME prop => Logic.mk_implies (Morphism.term const_morph
((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
val sup_of_classes = map (snd o rules thy) sups;
- val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
+ val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
val axclass_intro = #intro (AxClass.get_info thy class);
val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
val tac = REPEAT (SOMEGOAL