diff -r 52361140a0d1 -r c150e6fa4e0d lib/Tools/codegen
--- a/lib/Tools/codegen	Wed Mar 11 20:42:16 2009 +0100
+++ b/lib/Tools/codegen	Thu Mar 12 18:01:25 2009 +0100
@@ -33,8 +33,8 @@
 
 ## main
 
-THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end"
+CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
+CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
 
-echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE"
-exit ${PIPESTATUS[1]}
+"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1