diff -r 9644811b5b0a -r a2afc7ed2c68 lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Wed Apr 08 14:09:32 2020 +0200
+++ b/lib/scripts/getfunctions	Wed Apr 08 14:25:28 2020 +0200
@@ -113,22 +113,6 @@
 }
 export -f classpath
 
-#Isabelle/Scala tools
-function isabelle_scala_tools ()
-{
-  local X=""
-  for X in "$@"
-  do
-    if [ -z "$ISABELLE_SCALA_TOOLS" ]; then
-      ISABELLE_SCALA_TOOLS="$X"
-    else
-      ISABELLE_SCALA_TOOLS="$ISABELLE_SCALA_TOOLS:$X"
-    fi
-  done
-  export ISABELLE_SCALA_TOOLS
-}
-export -f isabelle_scala_tools
-
 #Isabelle fonts
 function isabelle_fonts ()
 {