1.1 --- a/src/Pure/Thy/thy_parse.ML	Sat Oct 18 13:23:02 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 20 10:38:16 1997 +0200
     1.3 @@ -413,9 +413,17 @@
     1.4    >> (fn ((x, y), z) => (cat_lines [x, y, z]));
     1.5  
     1.6  
     1.7 -(* global *)
     1.8 +(* local, global path *)
     1.9 +
    1.10 +val empty_decl = empty >> K "";
    1.11  
    1.12 -fun global_decl x = (empty >> K "\"/\"") x;
    1.13 +val global_path =
    1.14 +  "|> (fn thy => if ! global_names then thy else Theory.add_path \"/\" thy)";
    1.15 +
    1.16 +val local_path =
    1.17 +  global_path ^ "\n\
    1.18 +  \|> (fn thy => if ! global_names then thy\
    1.19 +  \ else Theory.add_path thy_name thy)";
    1.20  
    1.21  
    1.22  
    1.23 @@ -477,15 +485,16 @@
    1.24      \structure " ^ thy_name ^ " =\n\
    1.25      \struct\n\
    1.26      \\n\
    1.27 -    \local\n"
    1.28 +    \local\n\
    1.29 +    \ val thy_name = \"" ^ tname ^ "\";\n"
    1.30      ^ trfun_defs ^ "\n\
    1.31      \in\n\
    1.32      \\n"
    1.33      ^ mltxt ^ "\n\
    1.34      \\n\
    1.35      \val thy = thy\n\
    1.36 -    \\n" ^
    1.37 -    (if ! global_names then "" else "|> Theory.add_path " ^ quote tname ^ "\n") ^
    1.38 +    \\n"
    1.39 +    ^ local_path ^
    1.40      "\n\
    1.41      \|> Theory.add_trfuns\n"
    1.42      ^ trfun_args ^ "\n\
    1.43 @@ -531,8 +540,8 @@
    1.44  
    1.45  val pure_keywords =
    1.46   ["end", "ML", "mixfix", "infixr", "infixl", "binder", "global",
    1.47 -  "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
    1.48 -  "==", "=>", "<="];
    1.49 +  "local", "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]",
    1.50 +  "::", "==", "=>", "<="];
    1.51  
    1.52  val pure_sections =
    1.53   [section "classes" "|> Theory.add_classes" class_decls,
    1.54 @@ -549,7 +558,8 @@
    1.55    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.56    section "instance" "" instance_decl,
    1.57    section "path" "|> Theory.add_path" name,
    1.58 -  section "global" "|> Theory.add_path" global_decl];
    1.59 +  section "global" global_path empty_decl,
    1.60 +  section "local" local_path empty_decl];
    1.61  
    1.62  
    1.63  end;