# HG changeset patch
# User wenzelm
# Date 1218469068 -7200
# Node ID 03ed3519cf483156d6c9f68f974e7f2e8b5018c6
# Parent  4e50590ea9bcaddc2ccb5fac7fab69c97a8d2621
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!

diff -r 4e50590ea9bc -r 03ed3519cf48 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 11 14:50:04 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 11 17:37:48 2008 +0200
@@ -722,7 +722,7 @@
 val _ =
   OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
     (props_text >> (fn (pos, str) =>
-      Toplevel.no_timing o Toplevel.position pos o Toplevel.imperative (fn () =>
+      Toplevel.no_timing o Toplevel.imperative (fn () =>
         ignore (Isar.create_command (OuterSyntax.prepare_command pos str)))));
 
 val _ =