# 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