# HG changeset patch
# User haftmann
# Date 1283324614 -7200
# Node ID b912278b719fa8b031ac24e45f79b014fee19869
# Parent  68853347ba37cf166b3b29a704c7d902a2114fa3
repaired codegen tool

diff -r 68853347ba37 -r b912278b719f src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Wed Sep 01 08:52:49 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Wed Sep 01 09:03:34 2010 +0200
@@ -53,13 +53,13 @@
 
 if [ "$QUICK_AND_DIRTY" -eq 1 ]
 then
-  QND_CMD="set"
+  QND_FLAG="true"
 else
-  QND_CMD="reset"
+  QND_FLAG="false"
 fi
 
 CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
 
-FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
+FULL_CMD="quick_and_dirty := QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
 
 "$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1