better drop background syntax if entity depends on parameters;
more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);
#!/usr/bin/env bash
#
# Author: Makarius
#
# Default Isabelle application wrapper.
exec "$(dirname "$0")"/bin/isabelle jedit "$@"