tuned;

--- 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;

--- 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, []);