Isabelle.command: IsarCmd.nested_command (with properties);

--- a/src/Pure/Isar/isar_syn.ML	Wed Jan 02 23:00:52 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 02 23:00:54 2008 +0100
@@ -750,11 +750,9 @@
 
 val _ =
   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
-    (P.position P.string :|-- (fn (str, pos) =>
-      (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 msg)));
+    ((Scan.optional P.properties [] -- P.position P.string) :|-- (fn (props, arg) =>
+      Scan.succeed (K (IsarCmd.nested_command props arg))
+        handle ERROR msg => Scan.fail_with (K msg)));