locale_prefix: Sign.base_name;

--- a/src/Pure/Isar/proof.ML	Wed Nov 07 18:18:46 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Nov 07 18:53:11 2001 +0100
@@ -719,7 +719,8 @@
 (* global_qed *)
 
 fun locale_prefix None f thy = f thy
-  | locale_prefix (Some (loc, _)) f thy = thy |> Theory.add_path loc |> f |>> Theory.parent_path;
+  | locale_prefix (Some (loc, _)) f thy =
+      thy |> Theory.add_path (Sign.base_name loc) |> f |>> Theory.parent_path;
 
 fun locale_store_thm _ None _ = I
   | locale_store_thm name (Some (loc, atts)) th = Locale.store_thm loc ((name, th), atts);