diff -r 193c3ea0f63b -r cf8da9bbc584 lib/Tools/codegen
--- a/lib/Tools/codegen	Fri Sep 05 00:19:50 2008 +0200
+++ b/lib/Tools/codegen	Fri Sep 05 06:50:20 2008 +0200
@@ -35,6 +35,6 @@
 ## main
 
 CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-FULL_CMD="CodeTarget.shell_command \"$THY\" \"$CMD\";"
+FULL_CMD="Code_Target.shell_command \"$THY\" \"$CMD\";"
 
 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1