diff -r 862a20ffa8e2 -r c839a4c670c6 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -233,7 +233,7 @@
 fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
   let
     val intros = (snd o rules thy) sup :: map_filter I
-      [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
+      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
         (fst o rules thy) sub];
     val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
     val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))