# HG changeset patch
# User wenzelm
# Date 1199395513 -3600
# Node ID b626a630b2fc4b1b9be87ebf0fe0faab0471cff4
# Parent  d8e0190917a52db0550f26093d7eca0a71baf893
nested_command: simplified properties vs. position -- the latter also includes id now;

diff -r d8e0190917a5 -r b626a630b2fc src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Jan 03 22:25:12 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Jan 03 22:25:13 2008 +0100
@@ -392,9 +392,9 @@
 (* nested commands *)
 
 fun nested_command props (str, pos) =
-  let val (pos', props') = Position.of_properties (props @ Position.properties_of pos) in
+  let val pos' = Position.of_properties (props @ Position.properties_of pos) in
     (case OuterSyntax.parse pos' str of
-      [transition] => Toplevel.properties props' transition
+      [transition] => Toplevel.properties props transition
     | _ => error "exactly one command expected")
   end;