# HG changeset patch
# User haftmann
# Date 1254380996 -7200
# Node ID 06561afcadaa29335338e18b9b2ae410fe057509
# Parent  9b535493ac8d7fb36eedab1aa67b2b43fa92cb29
explicitly Unsynchronized

diff -r 9b535493ac8d -r 06561afcadaa src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Thu Oct 01 07:40:25 2009 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Thu Oct 01 09:09:56 2009 +0200
@@ -60,6 +60,6 @@
 
 CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
 
-FULL_CMD="$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
+FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
 
 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1