author | wenzelm |
Thu, 01 Nov 2001 21:12:13 +0100 (2001-11-01) | |
changeset 12017 | 78b8f9e13300 |
parent 12016 | 425289df84d3 |
child 12018 | ec054019c910 |
--- a/src/Pure/Thy/thy_parse.ML Thu Nov 01 21:11:52 2001 +0100 +++ b/src/Pure/Thy/thy_parse.ML Thu Nov 01 21:12:13 2001 +0100 @@ -562,7 +562,7 @@ section "local" "|> PureThy.local_path" empty_decl, section "setup" "|> Library.apply" long_id, section "MLtext" "" verbatim, - section "locale" "|> Locale.add_locale" locale_decl]; + section "locale" "|> Goals.add_locale" locale_decl]; end;