# HG changeset patch
# User wenzelm
# Date 1192547181 -7200
# Node ID 3bb2ad8b1b375d96409a9c57345e65a1463933dd
# Parent  b15a9a5dc9fe4a4f0a08ce3436c249d3b6ac7274
DeclareRobustCommand isascriptstyle (enables sub/superscripts within section headings etc.);

diff -r b15a9a5dc9fe -r 3bb2ad8b1b37 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Tue Oct 16 17:06:20 2007 +0200
+++ b/lib/texinputs/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
@@ -20,7 +20,7 @@
 %symbol markup -- \emph achieves decent spacing via italic corrections
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
-\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}