diff -r 42581956d75b -r 09b3010ffaf2 lib/Tools/java
--- a/lib/Tools/java	Sat Aug 16 13:32:23 2008 +0200
+++ b/lib/Tools/java	Sat Aug 16 14:29:25 2008 +0200
@@ -3,23 +3,7 @@
 # $Id$
 # Author: Makarius
 #
-# DESCRIPTION: Java wrapper
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [ARGS ...]"
-  echo
-  echo "  Invoke Java within the Isabelle environment."
-  echo
-  exit 1
-}
-
-
-## main
+# DESCRIPTION: invoke Java within the Isabelle environment
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 exec "$ISABELLE_JAVA" "$@"