diff -r d1c276b45dbc -r d5e76c2e335c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Nov 16 15:24:39 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Nov 16 15:25:17 2001 +0100
@@ -770,7 +770,8 @@
     val ts = flat tss;
     val locale_results =
       prep_result state ts raw_thm |> map (export goal_ctxt locale_ctxt);
-    val results = locale_results |> map (export locale_ctxt theory_ctxt);
+    val results = locale_results
+      |> map (Drule.strip_shyps_warning o export locale_ctxt theory_ctxt);
 
     val (k, locale, attss) =
       (case kind of Theorem x => x | _ => err_malformed "finish_global" state);