diff -r 02920bc314ee -r a3862cf94e73 lib/Tools/update_op
--- a/lib/Tools/update_op	Mon May 13 13:39:59 2019 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Tobias Nipkow, TU Muenchen
-#
-# DESCRIPTION: update "op _" syntax
-
-## diagnostics
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
-  echo
-  echo "  Options are:"
-  echo "    -m           ignore .ML files"
-  echo
-  echo "  Update the old \"op _\" syntax in theory and ML files."
-  echo
-  exit 1
-}
-
-
-IGNORE_ML=""
-
-while getopts "m" OPT
-do
-  case "$OPT" in
-    m)
-      IGNORE_ML="true"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-DIR="."
-if [ -n "$1" ]; then
-  DIR="$1"
-fi
-
-read -r -d '' THY_SCRIPT <<'EOF'
-# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
-s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
-# op *XY -> ( *XY)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
-# op *X -> ( *X)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
-# op *R -> ( *R)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
-# op *\<cdot> -> ( *\<cdot>)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
-# op ** -> ( ** )
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
-# op * -> ( * )
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
-# (op +) -> (+)
-s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
-# (op + -> ((+)
-s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
-# op + -> (+)
-s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
-s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
-# op+ -> (+)
-s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
-s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
-s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
-EOF
-
-read -r -d '' ML_SCRIPT <<'EOF'
-# op * -> ( * )
-s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
-s/"op[ ]*\*/"( \* )/g
-# (op +) -> (+)
-s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
-s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
-# (op + -> ((+)
-s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
-# op + -> (+)
-s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
-s/"op [ ]*\([^ )("]*\)/"(\1)/g
-# op+ -> (+)
-s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
-s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
-# is there \<...\> on the line (indicating Isabelle source):
-s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
-s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
-s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
-s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
-EOF
-
-find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;
-
-[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;
-