Sign.root_path, Sign.local_path;
authorwenzelm
Fri, 17 Jun 2005 18:33:40 +0200
changeset 16455 818303ef6940
parent 16454 af39c6510b86
child 16456 451f1c46d4ca
Sign.root_path, Sign.local_path;
src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Jun 17 18:33:39 2005 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Fri Jun 17 18:33:40 2005 +0200
@@ -557,8 +557,8 @@
   axm_section "axclass" "|> (#1 ooo AxClass.add_axclass)" axclass_decl,
   section "instance" "" instance_decl,
   section "path" "|> Theory.add_path" name,
-  section "global" "|> PureThy.global_path" empty_decl,
-  section "local" "|> PureThy.local_path" empty_decl,
+  section "global" "|> Sign.root_path" empty_decl,
+  section "local" "|> Sign.local_path" empty_decl,
   section "setup" "|> Library.apply" long_id,
   section "MLtext" "" verbatim,
   section "locale" "|> Goals.add_locale" locale_decl];