diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/symbolinput
--- a/lib/Tools/symbolinput	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/symbolinput	Fri Jan 02 13:24:53 1998 +0100
@@ -3,15 +3,5 @@
 # $Id$
 #
 # DESCRIPTION: translate symbols into \<...> sequences
-#
-# NOTE: If perl is unavailable we simply fall back on ucat!
 
-
-PERL=$(type -path perl)
-
-if [ -z "$PERL" ]
-then
-  exec $ISABELLE_HOME/lib/scripts/ucat "$@"
-else
-  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
-fi
+exec perl -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"