# HG changeset patch
# User wenzelm
# Date 1197146490 -3600
# Node ID 19cd3474fdf3de4e2cda0e5b62b0be3c07227295
# Parent  222b91dd754ce05465700abd13a51f372911abc2
tuned messages;

diff -r 222b91dd754c -r 19cd3474fdf3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Dec 08 21:20:07 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 08 21:41:30 2007 +0100
@@ -753,8 +753,8 @@
     (P.position P.string :|-- (fn (str, pos) =>
       (case OuterSyntax.parse pos str of
         [transition] => Scan.succeed (K transition)
-      | _ => Scan.fail_with (K "exactly one nested Isabelle command expected"))
-      handle ERROR msg => Scan.fail_with (K ("malformed nested command\n" ^ msg))));
+      | _ => Scan.fail_with (K "exactly one nested command expected"))
+      handle ERROR msg => Scan.fail_with (K ("malformed command\n" ^ msg))));