explicitly Unsynchronized
authorhaftmann
Thu, 01 Oct 2009 09:09:56 +0200
changeset 32806 06561afcadaa
parent 32805 9b535493ac8d
child 32807 c4f03b0cb753
child 32819 004b251ac927
child 32850 d95a7fd00bd4
explicitly Unsynchronized
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