# HG changeset patch
# User wenzelm
# Date 1218808262 -7200
# Node ID 7ed38f1d11de57dcc2fa2f5116adc91ef962d87c
# Parent  9f3fd48cf673a6dcea14bf92dc1044252e1551b0
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;

diff -r 9f3fd48cf673 -r 7ed38f1d11de src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Fri Aug 15 15:51:00 2008 +0200
+++ b/src/Pure/Syntax/simple_syntax.ML	Fri Aug 15 15:51:02 2008 +0200
@@ -24,6 +24,7 @@
   (case
       SymbolPos.explode (s, Position.none) |>
       Lexicon.tokenize lexicon false |>
+      filter Lexicon.is_proper |>
       Scan.read Lexicon.stopper scan of
     SOME x => x
   | NONE => error ("Malformed input: " ^ quote s));