src/Pure/Thy/thy_parse.ML
changeset 16455 818303ef6940
parent 15570 8d8c70b41bab
child 16486 1a12cdb6ee6b
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Jun 17 18:33:39 2005 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Jun 17 18:33:40 2005 +0200
     1.3 @@ -557,8 +557,8 @@
     1.4    axm_section "axclass" "|> (#1 ooo AxClass.add_axclass)" axclass_decl,
     1.5    section "instance" "" instance_decl,
     1.6    section "path" "|> Theory.add_path" name,
     1.7 -  section "global" "|> PureThy.global_path" empty_decl,
     1.8 -  section "local" "|> PureThy.local_path" empty_decl,
     1.9 +  section "global" "|> Sign.root_path" empty_decl,
    1.10 +  section "local" "|> Sign.local_path" empty_decl,
    1.11    section "setup" "|> Library.apply" long_id,
    1.12    section "MLtext" "" verbatim,
    1.13    section "locale" "|> Goals.add_locale" locale_decl];