# HG changeset patch
# User wenzelm
# Date 1361711647 -3600
# Node ID c68c1b89a0f1f2a1109f4570bc0f9d7d6b12477d
# Parent  3007d0bc9cb10af8172e6d5286dff847a13f625e
tuned;

diff -r 3007d0bc9cb1 -r c68c1b89a0f1 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Feb 24 14:11:51 2013 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Feb 24 14:14:07 2013 +0100
@@ -235,7 +235,7 @@
 fun basic_token pred (BasicToken tok) = pred tok
   | basic_token _ _ = false;
 
-val improper_token = basic_token (not o Token.is_proper);
+val improper_token = basic_token Token.is_improper;
 val comment_token = basic_token Token.is_comment;
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
diff -r 3007d0bc9cb1 -r c68c1b89a0f1 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 14:11:51 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 14:14:07 2013 +0100
@@ -118,7 +118,7 @@
 fun make_span toks =
   if not (null toks) andalso Token.is_command (hd toks) then
     Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks)
-  else if forall (not o Token.is_proper) toks then Span (Ignored, toks)
+  else if forall Token.is_improper toks then Span (Ignored, toks)
   else Span (Malformed, toks);
 
 fun flush (result, span) = if null span then (result, span) else (rev span :: result, []);