continued

--- a/doc-src/IsarImplementation/Thy/ML.thy	Mon Oct 22 21:32:12 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 23 10:53:15 2007 +0200
@@ -296,8 +296,6 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\
-  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
-  @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   \end{mldecls}
 *}
 
@@ -305,8 +303,6 @@
 typedecl foo
 consts foo :: foo
 ML {*
-val dummy_const = ("bar", @{typ foo}, NoSyn)
-val dummy_def = ("bar", @{term foo})
 val thy = Theory.copy @{theory}
 *}
 (*>*)
@@ -317,22 +313,30 @@
   particular value @{text "x \<Colon> foo"} which is then transformed
   by application of a function @{text "f \<Colon> foo \<Rightarrow> foo"},
   continued by an application of a function @{text "g \<Colon> foo \<Rightarrow> bar"},
-  and so on.  As a canoncial example, take primitive functions enriching
-  theories by constants and definitions:
-  @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory
--> theory"}
-  and @{ML "Theory.add_defs_i: bool -> bool
--> (bstring * term) list -> theory -> theory"}.
-  Written with naive application, an addition of a constant with
-  a corresponding definition would look like:
-  @{ML "Theory.add_defs_i false false [dummy_def]
-  (Sign.add_consts_i [dummy_const] thy)"}.
-  With increasing numbers of applications, this code gets quite unreadable.
-  Using composition, at least the nesting of brackets may be reduced:
-  @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i
-  [dummy_const]) thy"}.
-  What remains unsatisfactory is that things are written down in the opposite order
-  as they actually ``happen''.
+  and so on.  As a canoncial example, take functions enriching
+  a theory by constant declararion and primitive definitions:
+
+  \begin{quotation}
+    @{ML "Sign.declare_const: Markup.property list -> bstring * typ * mixfix
+       -> theory -> term * theory"}
+
+    @{ML "Thm.add_def: bool -> bstring * term -> theory -> thm * theory"}
+  \end{quotation}
+
+  Written with naive application, an addition of constant
+  @{text bar} with type @{typ "foo \<Rightarrow> foo"} and
+  a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
+
+  \begin{quotation}
+  @{ML "(fn (t, thy) => Thm.add_def false
+  (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
+    (Sign.declare_const []
+      (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}.
+  \end{quotation}
+
+  With increasing numbers of applications, this code gets quite
+  unreadable.  Further, it is unintuitive that things are
+  written down in the opposite order as they actually ``happen''.
 *}
 
 (*<*)
@@ -342,18 +346,15 @@
 (*>*)
 
 text {*
-  At this stage, Isabelle offers some combinators which allow for more convenient
-  notation, most notably reverse application:
-  @{ML "
-thy
-|> Sign.add_consts_i [dummy_const]
-|> Theory.add_defs_i false false [dummy_def]"}
-*}
-
-text {*
-  \noindent When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<Colon> 'a list"},
-  the @{ML fold} combinator lifts a single function @{text "f \<Colon> 'a -> 'b -> 'b"}:
-  @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"}
+  \noindent At this stage, Isabelle offers some combinators which allow
+  for more convenient notation, most notably reverse application:
+  \begin{quotation}
+@{ML "thy
+|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|> (fn (t, thy) => thy
+|> Thm.add_def false
+     (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
+  \end{quotation}
 *}
 
 text %mlref {*
@@ -362,12 +363,78 @@
   @{index_ML "op |>> ": "('a * 'c) * ('a -> 'b) -> 'b * 'c"} \\
   @{index_ML "op ||> ": "('c * 'a) * ('a -> 'b) -> 'c * 'b"} \\
   @{index_ML "op ||>> ": "('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b"} \\
+  \end{mldecls}
+*}
+
+text {*
+  \noindent Usually, functions involving theory updates also return
+  side results; to use these conveniently, yet another
+  set of combinators is at hand, most notably @{ML "op |->"}
+  which allows curried access to side results:
+  \begin{quotation}
+@{ML "thy
+|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|-> (fn t => Thm.add_def false
+      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+"}
+  \end{quotation}
+
+  \noindent @{ML "op |>>"} allows for processing side results on their own:
+  \begin{quotation}
+@{ML "thy
+|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
+|-> (fn def => Thm.add_def false (\"bar_def\", def))
+"}
+  \end{quotation}
+
+  \noindent Orthogonally, @{ML "op ||>"} applies a transformation
+  in the presence of side results which are left unchanged:
+  \begin{quotation}
+@{ML "thy
+|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+||> Sign.add_path \"foobar\"
+|-> (fn t => Thm.add_def false
+      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+||> Sign.restore_naming thy
+"}
+  \end{quotation}
+
+  \noindent @{index_ML "op ||>>"} accumulates side results:
+  \begin{quotation}
+@{ML "thy
+|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+||>> Sign.declare_const [] (\"foobar\", @{typ \"foo => foo\"}, NoSyn)
+|-> (fn (t1, t2) => Thm.add_def false
+      (\"bar_def\", Logic.mk_equals (t1, t2)))
+"}
+  \end{quotation}
+*}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
   \end{mldecls}
 *}
 
 text {*
-  \noindent FIXME transformations involving side results
+  \noindent This principles naturally lift to @{text lists} using
+  the @{ML fold} and @{ML fold_map} combinators.
+  The first lifts a single function
+  @{text "f \<Colon> 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"}
+  such that
+  @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"};
+  the second accumulates side results in a list by lifting
+  a single function
+  @{text "f \<Colon> 'a -> 'b -> 'c \<times> 'b"} to @{text "'a list -> 'b -> 'c list \<times> 'b"}
+  such that
+  @{text "y |> fold_map f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 ||>> f x\<^isub>2 ||>> \<dots> ||>> f x\<^isub>n
+    ||> (fn ((z\<^isub>1, z\<^isub>2), \<dots> z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \<dots> z\<^isub>n])"};
+
+  Example: FIXME
+  \begin{quotation}
+  \end{quotation}
 *}
 
 text %mlref {*
@@ -438,7 +505,7 @@
 
 text {*
   Lists are often used as set-like data structures -- set-like in
-  then sense that they support notion of @{ML member}-ship,
+  the sense that they support a notion of @{ML member}-ship,
   @{ML insert}-ing and @{ML remove}-ing, but are order-sensitive.
   This is convenient when implementing a history-like mechanism:
   @{ML insert} adds an element \emph{to the front} of a list,

--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Oct 22 21:32:12 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Oct 23 10:53:15 2007 +0200
@@ -339,8 +339,6 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
-  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
-  \indexml{fold-rev}\verb|fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -371,22 +369,30 @@
   particular value \isa{x\ {\isasymColon}\ foo} which is then transformed
   by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo},
   continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar},
-  and so on.  As a canoncial example, take primitive functions enriching
-  theories by constants and definitions:
-  \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory|\isasep\isanewline%
-\verb|-> theory|
-  and \verb|Theory.add_defs_i: bool -> bool|\isasep\isanewline%
-\verb|-> (bstring * term) list -> theory -> theory|.
-  Written with naive application, an addition of a constant with
-  a corresponding definition would look like:
-  \verb|Theory.add_defs_i false false [dummy_def]|\isasep\isanewline%
-\verb|  (Sign.add_consts_i [dummy_const] thy)|.
-  With increasing numbers of applications, this code gets quite unreadable.
-  Using composition, at least the nesting of brackets may be reduced:
-  \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i|\isasep\isanewline%
-\verb|  [dummy_const]) thy|.
-  What remains unsatisfactory is that things are written down in the opposite order
-  as they actually ``happen''.%
+  and so on.  As a canoncial example, take functions enriching
+  a theory by constant declararion and primitive definitions:
+
+  \begin{quotation}
+    \verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline%
+\verb|       -> theory -> term * theory|
+
+    \verb|Thm.add_def: bool -> bstring * term -> theory -> thm * theory|
+  \end{quotation}
+
+  Written with naive application, an addition of constant
+  \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
+  a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
+
+  \begin{quotation}
+  \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline%
+\verb|  ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
+\verb|    (Sign.declare_const []|\isasep\isanewline%
+\verb|      ("bar", @{typ "foo => foo"}, NoSyn) thy)|.
+  \end{quotation}
+
+  With increasing numbers of applications, this code gets quite
+  unreadable.  Further, it is unintuitive that things are
+  written down in the opposite order as they actually ``happen''.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -404,19 +410,15 @@
 \endisadelimML
 %
 \begin{isamarkuptext}%
-At this stage, Isabelle offers some combinators which allow for more convenient
-  notation, most notably reverse application:
-  \isasep\isanewline%
+\noindent At this stage, Isabelle offers some combinators which allow
+  for more convenient notation, most notably reverse application:
+  \begin{quotation}
 \verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.add_consts_i [dummy_const]|\isasep\isanewline%
-\verb||\verb,|,\verb|> Theory.add_defs_i false false [dummy_def]|%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\noindent When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list},
-  the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}:
-  \isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}%
+\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
+\verb||\verb,|,\verb|> Thm.add_def false|\isasep\isanewline%
+\verb|     ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
+  \end{quotation}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -432,6 +434,72 @@
   \indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
   \indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
   \indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+\noindent Usually, functions involving theory updates also return
+  side results; to use these conveniently, yet another
+  set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
+  which allows curried access to side results:
+  \begin{quotation}
+\verb|thy|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
+\verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
+
+  \end{quotation}
+
+  \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
+  \begin{quotation}
+\verb|thy|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn def => Thm.add_def false ("bar_def", def))|\isasep\isanewline%
+
+  \end{quotation}
+
+  \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
+  in the presence of side results which are left unchanged:
+  \begin{quotation}
+\verb|thy|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
+\verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
+
+  \end{quotation}
+
+  \noindent \indexml{op ||$>$$>$}\verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
+  \begin{quotation}
+\verb|thy|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ("foobar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false|\isasep\isanewline%
+\verb|      ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
+
+  \end{quotation}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
   \indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
   \end{mldecls}%
 \end{isamarkuptext}%
@@ -445,7 +513,21 @@
 \endisadelimmlref
 %
 \begin{isamarkuptext}%
-\noindent FIXME transformations involving side results%
+\noindent This principles naturally lift to \isa{lists} using
+  the \verb|fold| and \verb|fold_map| combinators.
+  The first lifts a single function
+  \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}
+  such that
+  \isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n};
+  the second accumulates side results in a list by lifting
+  a single function
+  \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ list\ {\isasymtimes}\ {\isacharprime}b}
+  such that
+  \isa{y\ {\isacharbar}{\isachargreater}\ fold{\isacharunderscore}map\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub n\ {\isacharbar}{\isacharbar}{\isachargreater}\ {\isacharparenleft}fn\ {\isacharparenleft}{\isacharparenleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharbrackright}{\isacharparenright}};
+
+  Example: FIXME
+  \begin{quotation}
+  \end{quotation}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -568,7 +650,7 @@
 %
 \begin{isamarkuptext}%
 Lists are often used as set-like data structures -- set-like in
-  then sense that they support notion of \verb|member|-ship,
+  the sense that they support a notion of \verb|member|-ship,
   \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive.
   This is convenient when implementing a history-like mechanism:
   \verb|insert| adds an element \emph{to the front} of a list,

--- a/doc-src/IsarImplementation/Thy/document/isabelle.sty	Mon Oct 22 21:32:12 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/isabelle.sty	Tue Oct 23 10:53:15 2007 +0200
@@ -25,10 +25,10 @@
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
-\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
+\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
+\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}