changeset 12071 | 3ef642b449da |
parent 12064 | 34c270893ecb |
child 12263 | 6f2acf10e2a2 |
--- 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 *)