diff -r 44d1f4e0a46e -r 15f4309bb9eb src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Apr 24 13:55:02 2012 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Apr 24 13:59:29 2012 +0100
@@ -8,10 +8,10 @@
 PRG="$(basename "$0")"
 
 function print_action_names() {
-  ACTIONS="$MIRABELLE_HOME/Actions/mirabelle_*.ML"
-  for ACTION in $ACTIONS
+  TOOLS="$MIRABELLE_HOME/Actions/mirabelle_*.ML"
+  for TOOL in $TOOLS
   do
-    echo $ACTION | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
+    echo $TOOL | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
   done
 }