nested_command: simplified properties vs. position -- the latter also includes id now;
--- 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;