--- a/src/Pure/Thy/thy_parse.ML Mon Oct 06 18:27:55 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML Mon Oct 06 18:29:11 1997 +0200
@@ -477,6 +477,7 @@
\\n"
^ extxt ^ "\n\
\\n\
+ \|> Theory.add_path \"/\"\n\
\|> Theory.add_name " ^ quote thy_name ^ ";\n\
\\n\
\val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
@@ -545,6 +546,7 @@
axm_section "defs" "|> Theory.add_defs" axiom_decls,
axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
- section "instance" "" instance_decl];
+ section "instance" "" instance_decl,
+ section "path" "|> Theory.add_path" name];
end;