# HG changeset patch
# User wenzelm
# Date 1218808252 -7200
# Node ID 76b51cd0a37cddea0d455371a208ca6d1c70b667
# Parent  10c927e4abf57ccb046c854313b81b235bf54595
renamed T.source_of' to T.source_position_of;

diff -r 10c927e4abf5 -r 76b51cd0a37c src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Fri Aug 15 15:50:50 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Fri Aug 15 15:50:52 2008 +0200
@@ -36,7 +36,7 @@
   val is_blank: token -> bool
   val is_newline: token -> bool
   val source_of: token -> string
-  val source_of': token -> SymbolPos.text * Position.T
+  val source_position_of: token -> SymbolPos.text * Position.T
   val content_of: token -> string
   val unparse: token -> string
   val text_of: token -> string * string
@@ -184,7 +184,7 @@
 fun source_of (Token ((source, (pos, _)), _, _)) =
   YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
 
-fun source_of' (Token ((source, (pos, _)), _, _)) = (source, pos);
+fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
 
 fun content_of (Token (_, (_, x), _)) = x;
 
diff -r 10c927e4abf5 -r 76b51cd0a37c src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Aug 15 15:50:50 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Aug 15 15:50:52 2008 +0200
@@ -117,7 +117,7 @@
       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if T.is_kind T.Verbatim tok then
       let
-        val (txt, pos) = T.source_of' tok;
+        val (txt, pos) = T.source_position_of tok;
         val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end