# HG changeset patch
# User wenzelm
# Date 1218109515 -7200
# Node ID 51c7b1baaf35f04a360262e18220c0c6d62320c9
# Parent  a52166b228b9ee21ba282dfed972549a76eb0b20
SymbolPos.explode;

diff -r a52166b228b9 -r 51c7b1baaf35 src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Thu Aug 07 13:45:13 2008 +0200
+++ b/src/Pure/Syntax/simple_syntax.ML	Thu Aug 07 13:45:15 2008 +0200
@@ -32,7 +32,7 @@
 
 fun read scan s =
   (case
-      Symbol.explode s |>
+      SymbolPos.explode (s, Position.none) |>
       Lexicon.tokenize lexicon false |>
       Scan.read stopper scan of
     SOME x => x