local section;
improved global, local;

--- a/src/Pure/Thy/thy_parse.ML	Sat Oct 18 13:23:02 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 20 10:38:16 1997 +0200
@@ -413,9 +413,17 @@
   >> (fn ((x, y), z) => (cat_lines [x, y, z]));
 
 
-(* global *)
+(* local, global path *)
+
+val empty_decl = empty >> K "";
 
-fun global_decl x = (empty >> K "\"/\"") x;
+val global_path =
+  "|> (fn thy => if ! global_names then thy else Theory.add_path \"/\" thy)";
+
+val local_path =
+  global_path ^ "\n\
+  \|> (fn thy => if ! global_names then thy\
+  \ else Theory.add_path thy_name thy)";
 
 
 
@@ -477,15 +485,16 @@
     \structure " ^ thy_name ^ " =\n\
     \struct\n\
     \\n\
-    \local\n"
+    \local\n\
+    \ val thy_name = \"" ^ tname ^ "\";\n"
     ^ trfun_defs ^ "\n\
     \in\n\
     \\n"
     ^ mltxt ^ "\n\
     \\n\
     \val thy = thy\n\
-    \\n" ^
-    (if ! global_names then "" else "|> Theory.add_path " ^ quote tname ^ "\n") ^
+    \\n"
+    ^ local_path ^
     "\n\
     \|> Theory.add_trfuns\n"
     ^ trfun_args ^ "\n\
@@ -531,8 +540,8 @@
 
 val pure_keywords =
  ["end", "ML", "mixfix", "infixr", "infixl", "binder", "global",
-  "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
-  "==", "=>", "<="];
+  "local", "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]",
+  "::", "==", "=>", "<="];
 
 val pure_sections =
  [section "classes" "|> Theory.add_classes" class_decls,
@@ -549,7 +558,8 @@
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   section "instance" "" instance_decl,
   section "path" "|> Theory.add_path" name,
-  section "global" "|> Theory.add_path" global_decl];
+  section "global" global_path empty_decl,
+  section "local" local_path empty_decl];
 
 
 end;