inner_syntax markup is back;
authorwenzelm
Thu, 07 Aug 2008 23:56:45 +0200
changeset 27788 5def98c2646b
parent 27787 3bff97077d26
child 27789 1bf827e3258d
inner_syntax markup is back;
src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Aug 07 23:32:49 2008 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Thu Aug 07 23:56:45 2008 +0200
@@ -141,8 +141,7 @@
 
 fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
 
-(*fun inner_syntax token = Scan.ahead token |-- not_eof >> T.source_of; FIXME tmp *)
-fun inner_syntax token = token;
+fun inner_syntax token = Scan.ahead token |-- not_eof >> T.source_of;
 
 fun kind k =
   group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);