# HG changeset patch
# User wenzelm
# Date 1005155591 -3600
# Node ID 8945a021f3752d7462b702340ed6b3a45f9c37d9
# Parent  935e29914f93d0c74d245d717b666d700fe1e236
locale_prefix: Sign.base_name;

diff -r 935e29914f93 -r 8945a021f375 src/Pure/Isar/proof.ML
--- 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);