locale_element/uses: string;
authorwenzelm
Tue, 06 Nov 2001 19:28:11 +0100
changeset 12071 3ef642b449da
parent 12070 c72fe1edc9e7
child 12072 4281198fb8cd
locale_element/uses: string;
src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Nov 06 19:27:56 2001 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Tue Nov 06 19:28:11 2001 +0100
@@ -313,7 +313,7 @@
   $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
     >> Locale.Defines ||
   $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) >> Locale.Notes ||
-  $$$ "uses" |-- (!!! ($$$ "FIXME" >> K ())) >> Locale.Uses);
+  $$$ "uses" |-- !!! xname >> Locale.Uses);
 
 
 (* proof methods *)