1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon May 25 21:25:04 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon May 25 21:27:22 1998 +0200
     1.3 @@ -188,6 +188,11 @@
     1.4  val name_list1 = names1 >> mk_list;
     1.5  
     1.6  
     1.7 +(* empty *)
     1.8 +
     1.9 +fun empty_decl toks = (empty >> K "") toks;
    1.10 +
    1.11 +
    1.12  (* classes *)
    1.13  
    1.14  val subclass = name -- optional ("<" $$-- !! name_list1) "[]";
    1.15 @@ -413,19 +418,6 @@
    1.16    >> (fn ((x, y), z) => (cat_lines [x, y, z]));
    1.17  
    1.18  
    1.19 -(* local, global path *)
    1.20 -
    1.21 -fun empty_decl toks = (empty >> K "") toks;
    1.22 -
    1.23 -val global_path =
    1.24 -  "|> (fn thy => if ! global_names then thy else Theory.root_path thy)";
    1.25 -
    1.26 -val local_path =
    1.27 -  global_path ^ "\n\
    1.28 -  \|> (fn thy => if ! global_names then thy\
    1.29 -  \ else Theory.add_path thy_name thy)";
    1.30 -
    1.31 -
    1.32  
    1.33  (** theory syntax **)
    1.34  
    1.35 @@ -491,17 +483,15 @@
    1.36      \structure " ^ thy_name ^ " =\n\
    1.37      \struct\n\
    1.38      \\n\
    1.39 -    \local\n\
    1.40 -    \ val thy_name = \"" ^ tname ^ "\";\n"
    1.41 +    \local\n"
    1.42      ^ local_defs ^ "\n\
    1.43      \in\n\
    1.44      \\n"
    1.45      ^ mltxt ^ "\n\
    1.46      \\n\
    1.47      \val thy = thy\n\
    1.48 -    \\n"
    1.49 -    ^ local_path ^
    1.50 -    "\n\
    1.51 +    \|> PureThy.put_name " ^ quote thy_name ^ "\n\
    1.52 +    \|> PureThy.local_path\n\
    1.53      \|> Theory.add_trfuns\n"
    1.54      ^ trfun_args ^ "\n\
    1.55      \|> Theory.add_trfunsT typed_print_translation\n\
    1.56 @@ -509,9 +499,9 @@
    1.57      \\n"
    1.58      ^ extxt ^ "\n\
    1.59      \\n\
    1.60 -    \|> Theory.add_name " ^ quote thy_name ^ ";\n\
    1.61 +    \|> PureThy.end_theory\n\
    1.62      \\n\
    1.63 -    \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.64 +    \val _ = store_theory thy;\n\
    1.65      \val _ = context thy;\n\
    1.66      \\n\
    1.67      \\n"
    1.68 @@ -566,8 +556,8 @@
    1.69    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.70    section "instance" "" instance_decl,
    1.71    section "path" "|> Theory.add_path" name,
    1.72 -  section "global" global_path empty_decl,
    1.73 -  section "local" local_path empty_decl,
    1.74 +  section "global" "|> PureThy.global_path" empty_decl,
    1.75 +  section "local" "|> PureThy.local_path" empty_decl,
    1.76    section "setup" "|> Theory.apply" long_id,
    1.77    section "MLtext" "" verbatim];
    1.78