# HG changeset patch
# User wenzelm
# Date 1005071291 -3600
# Node ID 3ef642b449da9017df3abdb6b41504167bdcaf15
# Parent  c72fe1edc9e7eba682f6a2f265589e3056d2d69a
locale_element/uses: string;

diff -r c72fe1edc9e7 -r 3ef642b449da 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 *)