# HG changeset patch
# User wenzelm
# Date 1218144769 -7200
# Node ID 3bff97077d2650a5d2568416a1889a647890ca1d
# Parent  4525c6f5d753dc7c75dcad74d491933c067330e1
disabled inner_syntax markup for now;

diff -r 4525c6f5d753 -r 3bff97077d26 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Aug 07 22:32:03 2008 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Thu Aug 07 23:32:49 2008 +0200
@@ -141,7 +141,8 @@
 
 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;
+(*fun inner_syntax token = Scan.ahead token |-- not_eof >> T.source_of; FIXME tmp *)
+fun inner_syntax token = token;
 
 fun kind k =
   group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);