# HG changeset patch # User wenzelm # Date 1119026020 -7200 # Node ID 818303ef694009dabc34865bfd3be9b0dd2cf9e1 # Parent af39c6510b86d85d274f408e501b14c65081ba9e Sign.root_path, Sign.local_path; diff -r af39c6510b86 -r 818303ef6940 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];