# HG changeset patch
# User wenzelm
# Date 1218808258 -7200
# Node ID 24b9f1d5824de05fe995eee47781b9b30922aa1e
# Parent  76b51cd0a37cddea0d455371a208ca6d1c70b667
renamed T.source_of' to T.source_position_of;
tuned signature;

diff -r 76b51cd0a37c -r 24b9f1d5824d src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Aug 15 15:50:52 2008 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Fri Aug 15 15:50:58 2008 +0200
@@ -7,7 +7,7 @@
 
 signature OUTER_PARSE =
 sig
-  type token
+  type token = OuterLex.token
   val group: string -> (token list -> 'a) -> token list -> 'a
   val !!! : (token list -> 'a) -> token list -> 'a
   val !!!! : (token list -> 'a) -> token list -> 'a
@@ -154,7 +154,7 @@
 val not_eof = RESET_VALUE (Scan.one T.not_eof);
 
 fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
-fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_of';
+fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
 fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
 
 fun kind k =