# HG changeset patch
# User wenzelm
# Date 1393188781 -3600
# Node ID e42e5671612c2e116ae6a67e10e5379704eb417e
# Parent  abec82f4e3e92add19146a1c172431230f5c07d3
tuned message;

diff -r abec82f4e3e9 -r e42e5671612c src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun Feb 23 21:45:27 2014 +0100
+++ b/src/Pure/Isar/args.ML	Sun Feb 23 21:53:01 2014 +0100
@@ -291,8 +291,8 @@
   (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
     (SOME x, (st', [])) => (x, st')
   | (_, (_, args')) =>
-      error (kind ^ " " ^ quote s ^ Position.here pos ^ ": bad arguments\n  " ^
-        space_implode " " (map Token.unparse args')));
+      error (kind ^ " " ^ quote s ^ Position.here pos ^ ": bad arguments" ^
+        (if null args' then "" else "\n  " ^ space_implode " " (map Token.unparse args'))));
 
 fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;