nested commands: avoid nested errors;

--- a/src/Pure/Isar/isar_syn.ML	Fri Dec 14 17:56:08 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 14 17:57:39 2007 +0100
@@ -754,7 +754,7 @@
       (case OuterSyntax.parse pos str of
         [transition] => Scan.succeed (K transition)
       | _ => Scan.fail_with (K "exactly one command expected"))
-      handle ERROR msg => Scan.fail_with (K ("malformed command\n" ^ msg))));
+      handle ERROR msg => Scan.fail_with (K msg)));
 
 
 

--- a/src/Pure/Isar/outer_parse.ML	Fri Dec 14 17:56:08 2007 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Dec 14 17:57:39 2007 +0100
@@ -113,7 +113,9 @@
       | get_pos (tok :: _) = T.pos_of tok;
 
     fun err (toks, NONE) = kind ^ get_pos toks
-      | err (toks, SOME msg) = kind ^ get_pos toks ^ ": " ^ msg;
+      | err (toks, SOME msg) =
+          if String.isPrefix kind msg then msg
+          else kind ^ get_pos toks ^ ": " ^ msg;
   in Scan.!! err scan end;
 
 fun !!! scan = cut "Outer syntax error" scan;