src/HOL/Mirabelle/lib/Tools/mirabelle

 
 
 PRG="$(basename "$0")"
 
 function print_action_names() {
-  TOOLS="$MIRABELLE_HOME/Actions/mirabelle_*.ML"
+  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
   for TOOL in $TOOLS
   do
     echo $TOOL | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
   done
 }
 
 function print_sledgehammer_options() {
-  grep -e "^val .*K =" $MIRABELLE_HOME/Actions/mirabelle_sledgehammer.ML \
+  grep -e "^val .*K =" $MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML \
   | perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/    $1$2/'
 }
 
 function usage() {
   [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"