proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);

--- a/lib/texinputs/isabelle.sty	Tue Aug 02 21:30:30 2016 +0200
+++ b/lib/texinputs/isabelle.sty	Tue Aug 02 21:55:15 2016 +0200
@@ -73,6 +73,7 @@
 \newcommand{\isadigit}[1]{#1}
 
 \newcommand{\isachardefaults}{%
+\def\isacharbell{\isamath{\bigbox}}  %requires stmaryrd
 \chardef\isacharbang=`\!%
 \chardef\isachardoublequote=`\"%
 \chardef\isachardoublequoteopen=`\"%

--- a/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Aug 02 21:30:30 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Aug 02 21:55:15 2016 +0200
@@ -1,6 +1,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage{amsmath}
+\usepackage{stmaryrd}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

--- a/src/Pure/Thy/latex.ML	Tue Aug 02 21:30:30 2016 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Aug 02 21:55:15 2016 +0200
@@ -45,7 +45,8 @@
 
 val char_table =
   Symtab.make
-   [("!", "{\\isacharbang}"),
+   [("\007", "{\\isacharbell}"),
+    ("!", "{\\isacharbang}"),
     ("\"", "{\\isachardoublequote}"),
     ("#", "{\\isacharhash}"),
     ("$", "{\\isachardollar}"),