\newcommand{\ml}[1]{{\tt #1}}
\renewcommand{\cdots}{\mbox{$\cdot\!\cdot\!\cdot$}}

        % Core Language
\newcommand{\ttlbrace}{\mbox{\tt\char'173}}
\newcommand{\ttrbrace}{\mbox{\tt\char'175}}
\newcommand{\lttbrace}{\mbox{\tt\char'173}}
\newcommand{\rttbrace}{\mbox{\tt\char'175}}
\newcommand{\ttprime}{\mbox{\tt\char'047}}
\newcommand{\ABSTYPE}{{\tt abstype}}
\newcommand{\AND }{{\tt and}}
\newcommand{\ANDALSO }{{\tt andalso}}
\newcommand{\AS}{{\tt as}}
\newcommand{\CASE}{{\tt case}}
\newcommand{\DO}{{\tt do}}
\newcommand{\DATATYPE}{{\tt datatype}}
\newcommand{\ELSE}{{\tt else}}
\newcommand{\END}{{\tt end}}
\newcommand{\EXCEPTION}{{\tt exception}}
\newcommand{\FUN}{{\tt fun}}
\newcommand{\FN}{{\tt fn}}
\newcommand{\HANDLE}{{\tt handle}}
\newcommand{\IF}{{\tt if}}
\newcommand{\IN}{{\tt in}}
\newcommand{\INFIX}{{\tt infix}}
\newcommand{\INFIXR}{{\tt infixr}}
\newcommand{\LET}{{\tt let}}
\newcommand{\LOCAL}{{\tt local}}
\newcommand{\NONFIX}{{\tt nonfix}}
\newcommand{\OF}{{\tt of}}
\newcommand{\OP}{{\tt op}}
\newcommand{\ORELSE}{{\tt orelse}}
\newcommand{\RAISE}{{\tt raise}}
\newcommand{\REC}{{\tt rec}}
\newcommand{\THEN}{{\tt then}}
\newcommand{\TYPE}{{\tt type}}
\newcommand{\VAL}{{\tt val}}
\newcommand{\WITH}{{\tt with}}
\newcommand{\WITHTYPE}{{\tt withtype}}
\newcommand{\WHILE}{{\tt while}}

        % Modules
\newcommand{\EQTYPE}{\ml{eqtype}}
\newcommand{\FUNCTOR}{\ml{functor}}
\newcommand{\INCLUDE}{\ml{include}}
\newcommand{\SIG}{\ml{sig}}
\newcommand{\OPEN}{\ml{open}}
\newcommand{\SHARING}{\ml{sharing}}
\newcommand{\SIGNATURE}{\ml{signature}}
\newcommand{\STRUCT}{\ml{struct}}
\newcommand{\STRUCTURE}{\ml{structure}}
          % Identifier class names
\newcommand{\Var}{{\rm Var}}
\newcommand{\Con}{{\rm Con}}
\newcommand{\SCon}{{\rm SCon}}
\newcommand{\Exn}{{\rm ExCon}}
\newcommand{\TyVar}{{\rm TyVar}}
\newcommand{\ImpTyVar}{{\rm ImpTyVar}}
\newcommand{\AppTyVar}{{\rm AppTyVar}}
\newcommand{\TyCon}{{\rm TyCon}}
\newcommand{\Lab}{{\rm Lab}}
\newcommand{\StrId}{{\rm StrId}}
\newcommand{\FunId}{{\rm FunId}}
\newcommand{\SigId}{{\rm SigId}}

          % Identifier class variables
\newcommand{\id}{{\it id}}
\newcommand{\var}{{\it var}}
\newcommand{\con}{{\it con}}
\newcommand{\scon}{{\it scon}}
\newcommand{\exn}{{\it excon}}
\newcommand{\tyvar}{{\it tyvar}}
\newcommand{\atyvar}{\mbox{\tt \ttprime a}}
\newcommand{\btyvar}{\mbox{\tt \ttprime b}}
\newcommand{\ctyvar}{\mbox{\tt \ttprime c}}
\newcommand{\aityvar}{\mbox{\tt \ttprime\_a}}
\newcommand{\aetyvar}{\mbox{\tt \ttprime\ttprime a}}
\newcommand{\tycon}{{\it tycon}}
\newcommand{\lab}{{\it lab}}
\newcommand{\strid}{{\it strid}}

\newcommand{\longvar}{{\it longvar}}
\newcommand{\longcon}{{\it longcon}}
\newcommand{\longexn}{{\it longexcon}}
\newcommand{\longtycon}{{\it longtycon}}
\newcommand{\longstrid}{{\it longstrid}}

          % General classes
\newcommand{\phrase}{{\it phrase}}

          % Core Syntax Classes
\newcommand{\apexp}{{\it appexp}}
\newcommand{\atpat}{{\it atpat}}
\newcommand{\atexp}{{\it atexp}}
\newcommand{\bind}{{\it bind}}
\newcommand{\constrs}{{\it conbind}}
\newcommand{\ConBind}{{\rm ConBind}}
\newcommand{\datbind}{{\it datbind}}
\newcommand{\dec}{{\it dec}}
\newcommand{\dir}{{\it dir}}
\newcommand{\exnbind}{{\it exbind}}
\renewcommand{\exp}{{\it exp}}
\newcommand{\fvalbind}{{\it fvalbind}}
\newcommand{\handler}{{\it handler}}
\newcommand{\hanrule}{{\it hrule}}
\newcommand{\inexp}{{\it infexp}}
\newcommand{\labexps}{{\it exprow}}
\newcommand{\labpats}{{\it patrow}}
\newcommand{\labtys}{{\it tyrow}}
\newcommand{\match}{{\it match}}
\newcommand{\pat}{{\it pat}}
\newcommand{\mrule}{{\it mrule}}
\newcommand{\ty}{{\it ty}}
    \newcommand{\tyb}{\mbox{$\ty^\bullet$}}
\newcommand{\tyseq}{{\it tyseq}}
\newcommand{\tyvarseq}{{\it tyvarseq}}
\newcommand{\typbind}{{\it typbind}}
\newcommand{\valbind}{{\it valbind}}

 % ranged over by the variables




       % Modules syntax classes

\newcommand{\datdesc}{{\it datdesc}}
\newcommand{\condesc}{{\it condesc}}
\newcommand{\exndesc}{{\it exdesc}}
\newcommand{\funbind}{{\it funbind}}
\newcommand{\fundec}{{\it fundec}}
\newcommand{\fundesc}{{\it fundesc}}
\newcommand{\funid}{{\it funid}}
\newcommand{\funsigexp}{{\it funsigexp}}
\newcommand{\funspec}{{\it funspec}}
\newcommand{\funtyp}{{\it funtyp}}
\newcommand{\longstridk}{\strid_1.\cdots.\strid_k}
\newcommand{\longtyconk}{\strid_1.\cdots.\strid_k.\tycon}
\newcommand{\topdec}{{\it topdec}}
\newcommand{\program}{{\it program}}
\newcommand{\sigid}{{\it sigid}}
\newcommand{\shareq}{{\it shareq}}
\newcommand{\sigbind}{{\it sigbind}}
\newcommand{\sigdec}{{\it sigdec}}
\newcommand{\sigexp}{{\it sigexp}}
\newcommand{\spec}{{\it spec}}
\newcommand{\strbind}{{\it strbind}}
\newcommand{\strdec}{{\it strdec}}
\newcommand{\strexp}{{\it strexp}}
\newcommand{\strdesc}{{\it strdesc}}
\newcommand{\typdesc}{{\it typdesc}}
\newcommand{\valdesc}{{\it valdesc}}
           % Core Language Phrases

           % Expressions

\newcommand{\recexp}{\mbox{$\langle\labexps\rangle$}}
\newcommand{\longlabexps}{\mbox{\lab\ \ml{=} \exp\
                          $\langle$ \ml{,} \labexps$\rangle$}}
\newcommand{\parexp}{\mbox{\ml{(} \exp\ \ml{)}}}
\newcommand{\appexp}
           {\mbox{\exp\ \atexp}}
\newcommand{\infexp}
           {\mbox{$\exp_1\ \id\ \exp_2$}}
\newcommand{\opp}
           {\mbox{$\langle\OP\rangle$}}
\newcommand{\typedexp}
           {\mbox{\exp\ \ml{:} \ty}}
\newcommand{\handlexp}
           {\mbox{\exp\ \HANDLE\ \match}}
\newcommand{\raisexp}
           {\mbox{\RAISE\ \exp}}
\newcommand{\letexp}
           {\mbox{\LET\ \dec\ \IN\ \exp\ \END}}
\newcommand{\fnexp}
           {\mbox{\FN\ \match}}
\newcommand{\fnexpb}
           {\FN\ \match^\bullet}

           % Matches and Handlers
\newcommand{\longmatch}
           {\mbox{\mrule\ $\langle$ \ml{|} \match$\rangle$}}
\newcommand{\longmatcha}
           {\mbox{\mrule\ \ml{|} \match}}
\newcommand{\longmrule}
           {\mbox{\pat\ \ml{=>} \exp}}
\newcommand{\longhandler}
           {\mbox{\hanrule\ $\langle$ \ml{||} \handler$\rangle$}}
\newcommand{\longhandlera}
           {\mbox{\hanrule\ \ml{||} \handler}}
\newcommand{\longhanrule}
           {\mbox{\longexn\ \WITH\ \match}}
\newcommand{\lasthanrule}
           {\mbox{? \ml{=>} \exp}}

          % Declarations
\newcommand{\valdec}
           {\mbox{\VAL\ \valbind}}
\newcommand{\valdecS}
           {\mbox{$\VAL_{\U}$\ \valbind}}
\newcommand{\typedec}
           {\mbox{\TYPE\ \typbind}}
\newcommand{\datatypedec}
           {\mbox{\DATATYPE\ \datbind}}
\newcommand{\datatypedeca}
           {\mbox{\DATATYPE\ \datbind\ $\langle\WITHTYPE\ \typbindb\rangle$}}
\newcommand{\abstypedec}
           {\mbox{\ABSTYPE\ \datbind\ \WITH\ \dec\ \END}}
\newcommand{\abstypedeca}
           {\mbox{\ABSTYPE\ \datbind\ $\langle\WITHTYPE\ \typbindb\rangle$}}
\newcommand{\exceptiondec}
           {\mbox{\EXCEPTION\ \exnbind}}
\newcommand{\localdec}
           {\mbox{\LOCAL\ $\dec_1$\ \IN\ $\dec_2$\ \END}}
\newcommand{\emptydec}
           {\mbox{\qquad}}
\newcommand{\seqdec}
           {\mbox{$\dec_1\ \langle\ml{;}\rangle\ \dec_2$}}
\newcommand{\longinfix}
           {\mbox{$\INFIX\ \langle d\rangle\ \id_1\ \cdots\ \id_n$}}
\newcommand{\longinfixr}
           {\mbox{$\INFIXR\ \langle d\rangle\ \id_1\ \cdots\ \id_n$}}
\newcommand{\longnonfix}
           {\mbox{$\NONFIX\ \id_1\ \cdots\ \id_n$}}

          % Bindings
\newcommand{\longvalbind}
           {\mbox{\pat\ \ml{=} \exp\ $\langle\AND\ \valbind\rangle$}}
\newcommand{\recvalbind}
           {\mbox{\REC\ \valbind}}
\newcommand{\longtypbind}
           {\mbox{\tyvarseq\ \tycon\ \ml{=} \ty
            \ $\langle\AND\ \typbind\rangle$}}
\newcommand{\longdatbind}
           {\mbox{\tyvarseq\ \tycon\ \ml{=} \constrs
                  \ $\langle\AND\ \datbind\rangle$}}
\newcommand{\longconstrs}
           {\mbox{$\con\ \langle\OF\ \ty\rangle\
                   \langle$ \ml{|} \constrs$\rangle$}}
\newcommand{\longerconstrs}
           {\mbox{$\con\ \langle\OF\ \ty\rangle\
                   \langle\langle$ \ml{|} \constrs$\rangle\rangle$}}
% \newcommand{\generativeexnbind}
%            {\mbox{$\langle\OP\rangle\exn\ \langle\OF\ \ty\rangle\
%                    \langle\AND\ \exnbind\rangle$}}
% \newcommand{\eqexnbind}
%            {\mbox{$\langle\OP\rangle$\exn\ \ml{=} 
%                   $\langle\OP\rangle\longexn\ 
%                   \langle\AND\ \exnbind\rangle$}}
\newcommand{\generativeexnbind}
           {\mbox{$\exn\ \langle\OF\ \ty\rangle\
                   \langle\AND\ \exnbind\rangle$}}
\newcommand{\eqexnbind}
           {\mbox{$\exn\ \EQ\ \longexn\ 
                  \langle\AND\ \exnbind\rangle$}}
\newcommand{\longexnbinda}
           {\mbox{\exn\ $\langle\OF\ \ty\rangle$\ 
                  $\langle\langle\AND\ \exnbind\rangle\rangle$}}
\newcommand{\longexnbindaa}
           {\mbox{\exn\
                  $\langle\AND\ \exnbind\rangle$}}
\newcommand{\longexnbindb}
           {\mbox{\exn\ \ml{=}\ \longexn\ $\langle\AND\ \exnbind\rangle$}}
% from version 1:
%\newcommand{\longexnbind}
%           {\mbox{\exn\ $\langle$\ml{:} $\ty\rangle
%                  \langle$\ml{=} $\longexn\rangle
%                  \ \langle\AND\ \exnbind\rangle$}}
%\newcommand{\longexnbinda}
%           {\mbox{\exn\ $\langle$\ml{:} $\ty\rangle
%                  \ \langle\langle\AND\ \exnbind\rangle\rangle$}}
%\newcommand{\longexnbindaa}
%           {\mbox{\exn\
%                  $\langle\AND\ \exnbind\rangle$}}
%\newcommand{\longexnbindb}
%           {\mbox{\exn\ $\langle$\ml{:} $\ty\rangle
%                  \ $\ml{=} $\longexn
%                  \ \langle\langle\AND\ \exnbind\rangle\rangle$}}
%\newcommand{\longexnbindbb}
%           {\mbox{\exn\ \ml{=} \longexn\
%                  $\langle\AND\ \exnbind\rangle$}}

          % Patterns
\newcommand{\wildpat}{\mbox{\ml{\_}}}
\newcommand{\recpat}{\mbox{$\langle\labpats\rangle$}}
\newcommand{\wildrec}{\mbox{\ml{...}}}
\newcommand{\longlabpats}{\mbox{\lab\ \ml{=} \pat\
                          $\langle$ \ml{,} \labpats$\rangle$}}
\newcommand{\parpat}{\mbox{\ml{(} \pat\ \ml{)}}}
\newcommand{\conpat}
           {\mbox{\longcon\ \atpat}}
\newcommand{\exconpat}
           {\mbox{\longexn\ \atpat}}
\newcommand{\infpat}
           {\mbox{$\pat_1\ \con\ \pat_2$}}
\newcommand{\infexpat}
           {\mbox{$\pat_1\ \exn\ \pat_2$}}
\newcommand{\typedpat}
           {\mbox{\pat\ \ml{:} \ty}}
\newcommand{\layeredpat}
           {\mbox{\var$\langle$\ml{:} \ty$\rangle$ \AS\ \pat}}
\newcommand{\layeredpata}
           {\mbox{\var\ \AS\ \pat}}

          % Types
\newcommand{\rectype}{\mbox{$\langle\labtys\rangle$}}
\newcommand{\longlabtys}{\mbox{\lab\ \ml{:} \ty\
                          $\langle$ \ml{,} \labtys$\rangle$}}
\newcommand{\constype}
           {\mbox{\tyseq\ \longtycon}}
\newcommand{\funtype}
           {\mbox{\ty\ \ml{->} \ty$'$}}
\newcommand{\partype}{\mbox{\ml{(} \ty\ \ml{)}}}
\newcommand{\longtyseq}{\mbox{\ml{(} $\ty_1,\cdots\,\ty_k$ \ml{)}}}
\newcommand{\longtyvarseq}{\mbox{\ml{(} $\tyvar_1,\cdots,\tyvar_k$ \ml{)}}}

        % Modules Phrases

\newcommand{\emptyphrase}{\qquad}


    	% structure-level declarations

\newcommand{\singstrdec}{\mbox{$\STRUCTURE\ \strbind $}}
\newcommand{\localstrdec}{\mbox{$\LOCAL\ \strdec_1\ \IN\ \strdec_2\ \END $}}
\newcommand{\openstrdec}{\mbox{$\OPEN\ \longstrid_1\ \cdots\ \longstrid_n $}}
\newcommand{\emptystrdec}{\emptyphrase}
\newcommand{\seqstrdec}{\mbox{$\strdec_1\ \langle$\ml{;}$\rangle\ \strdec_2 $}}


        % structure bindings

\newcommand{\strbinder}
           {\mbox{$\strid\ \langle$\ml{:}$\ \sigexp\rangle$
            \ml{=} $\strexp\ \langle\langle\AND\ \strbind\rangle\rangle$}}
\newcommand{\strbindera}
           {\mbox{$\strid\ \langle$\ml{:}$\ \sigexp\rangle$
            \ml{=} $\strexp\ \langle\AND\ \strbind\rangle$}}


	% structure expressions

\newcommand{\encstrexp}{\mbox{\STRUCT\ \strdec\ \END}}
\newcommand{\funappdec}{\mbox{\funid\ \ml{(}\ \strdec\ \ml{)} }}
\newcommand{\funappstr}{\mbox{\funid\ \ml{(}\ \strexp\ \ml{)} }}
\newcommand{\letstrexp}{\mbox{\LET\ \strdec\ \IN\ \strexp\ \END}}

        % specifications

\newcommand{\valspec}{\mbox{\VAL\ \valdesc}}
\newcommand{\typespec}{\mbox{\TYPE\ \typdesc}}
\newcommand{\eqtypespec}{\mbox{\EQTYPE\ \typdesc}}
\newcommand{\datatypespec}{\mbox{\DATATYPE\ \datdesc}}
\newcommand{\exceptionspec}{\mbox{\EXCEPTION\ \exndesc}}
\newcommand{\structurespec}{\mbox{\STRUCTURE\ \strdesc}}
\newcommand{\sharingspec}{\mbox{\SHARING\ \shareq}}
\newcommand{\localspec}{\mbox{$\LOCAL\ \spec_1\ \IN\ \spec_2\ \END$}}
\newcommand{\openspec}{\mbox{$\OPEN\ \longstrid_1\ \cdots\ \longstrid_n $}}
\newcommand{\emptyspec}{\emptyphrase}
\newcommand{\seqspec}{\mbox{$\spec_1\ \langle$\ml{;}$\rangle\ \spec_2$}}
\newcommand{\inclspec}{\mbox{$\INCLUDE\ \sigid_1\ \cdots\ \sigid_n $}}


        % descriptions

\newcommand{\valdescription}
           {\mbox{\var\ \ml{:} $\ty\ \langle\AND\ \valdesc\rangle$}}

\newcommand{\typdescription}
           {\mbox{\tyvarseq\ \tycon\ $\langle\AND\ \typdesc\rangle$}}

\newcommand{\datdescription}
           {\mbox{\tyvarseq\ \tycon\ \ml{=} \condesc
             \ $\langle\AND\ \datdesc\rangle$}}

\newcommand{\condescription}
           {\mbox{$\con\ \langle\OF\ \ty\rangle\
                   \langle$ \ml{|} \condesc$\rangle$}}

\newcommand{\longcondescription}
           {\mbox{$\con\ \langle\OF\ \ty\rangle\
                   \langle\langle$ \ml{|} \condesc$\rangle\rangle$}}

\newcommand{\exndescription}
           {\mbox{\exn\ $\langle\OF\ \ty\rangle$
            \ $\langle\AND\ \exndesc\rangle$}}

\newcommand{\exndescriptiona}
           {\mbox{\exn\ $\langle\OF\ \ty\rangle$
            \ $\langle\langle\AND\ \exndesc\rangle\rangle$}}

\newcommand{\strdescription}
           {\mbox{\strid\ \ml{:} \sigexp
            \ $\langle\AND\ \strdesc\rangle$}}

        % sharing equations

\newcommand{\strshareq}{\mbox{$\longstrid_1$ \ml{=} $\cdots$
                                             \ml{=} $\longstrid_n$ }}
\newcommand{\typshareq}{\mbox{$\TYPE\ \longtycon_1$ \ml{=} $\cdots$
                                                    \ml{=} $\longtycon_n$ }}
\newcommand{\multshareq}{\mbox{$\shareq_1\ \AND\ \shareq_2$}}


	% signature expressions

\newcommand{\encsigexp}{\mbox{\SIG\ \spec\ \END}}

        % signature declarations

\newcommand{\singsigdec}{\mbox{$\SIGNATURE\ \sigbind $}}
\newcommand{\emptysigdec}{\emptyphrase}
\newcommand{\seqsigdec}{\mbox{$\sigdec_1\ \langle$\ml{;}$\rangle\ \sigdec_2 $}}


        % signature bindings

%%% SMK replaced sigexp by psigexp
\newcommand{\sigbinder}
           {\mbox{\sigid\ \ml{=} \psigexp
            \ $\langle\AND\ \sigbind\rangle$}}


        % functor declarations

\newcommand{\singfundec}{\mbox{$\FUNCTOR\ \funbind $}}
\newcommand{\emptyfundec}{\emptyphrase}
\newcommand{\seqfundec}{\mbox{$\fundec_1\ \langle$\ml{;}$\rangle\ \fundec_2 $}}


        % functor bindings

\newcommand{\funbinder}
           {\mbox{\funid\ \ml{(} \spec\ \ml{)}
                          $\langle$\ml{:}$\ \sigexp\rangle$\ \ml{=} $\strexp$
                          $\langle\langle\AND\ \funbind\rangle\rangle$}}
\newcommand{\funbindera}
           {\mbox{\funid\ \ml{(} \spec\ \ml{)}
                          $\langle$\ml{:}$\ \sigexp\rangle$\ \ml{=} $\strexp$}}
\newcommand{\funstrbinder}
           {\mbox{\funid\ \ml{(}\ \strid\ \ml{:}\ \sigexp\ \ml{)}
                        $\langle$\ml{:}$\ \sigexp'\rangle$\ \ml{=} $\strexp$}}
\newcommand{\optfunbind}
           {\mbox{$\langle\langle\AND\ \funbind\rangle\rangle$}}
\newcommand{\optfunbinda}
           {\mbox{$\langle\AND\ \funbind\rangle$}}
\newcommand{\funstrbindera}
           {\mbox{\funid\ \ml{(}\ \strid\ \ml{)}\ \ml{=} \strexp
            \ $\langle\AND\ \funbind\rangle$}}


        %functor signature expressions
%%% SMK: replaced sigexp by psigexp
\newcommand{\longfunsigexp}
           {\mbox{\ml{(}\ \spec\ \ml{)}
                          \ml{:}\ \psigexp}}
\newcommand{\longfunsigexpa}
           {\mbox{\ml{(}\ \strid\ \ml{:}\ \psigexp\ \ml{)}
                          \ml{:}\ \psigexp$'$}}


        % functor specifications

\newcommand{\singfunspec}{\mbox{\FUNCTOR\ \fundesc}}
\newcommand{\emptyfunspec}{\emptyphrase}
\newcommand{\seqfunspec}
           {\mbox{$\funspec_1\ \langle$\ml{;}$\rangle\ \funspec_2$}}
 

        % functor descriptions

\newcommand{\longfundesc}
           {\mbox{\funid\ \funsigexp\ $\langle\AND\ \fundesc\rangle$}}


	% programs
\newcommand{\longprog}{\mbox{\topdec\ \ml{;}\ $\langle\program\rangle$}}
\newcommand{\seqprog}
 {\mbox{$\program_1\ \langle$\ml{;}$\rangle\ \program_2$}}
% **************** END SYNTAX *************************
\newcommand{\ML}{{\rm ML}}


% 	finite sets and maps (assume math mode)
%
\newcommand{\Fin}{\mathop{\rm Fin}\nolimits}
\newcommand{\Dom}{\mathop{\rm Dom}\nolimits}
\newcommand{\Ran}{\mathop{\rm Ran}\nolimits}
\newcommand{\finfun}[2]{#1\stackrel{{\rm fin}}{\to}#2}
\newcommand{\emptymap}{\{\}}
\newcommand{\kmap}[2]{\{#1_1\mapsto#2_1,\cdots,#1_k\mapsto#2_k\}}
\newcommand{\plusmap}[2]{#1 + #2}
%
\newcommand{\TyVarSet}{{\rm TyVarSet}}
%
%
%	Names     (assume math mode)
\newcommand{\TyNames}{{\rm TyName}}
\newcommand{\TyNameSets}{{\rm TyNameSet}}
\newcommand{\StrNames}{{\rm StrName}}
\newcommand{\StrNameSets}{{\rm StrNameSet}}

\newcommand{\NameSets}{{\rm NameSet}}
\newcommand{\TyNamesk}{\TyNames^{(k)}}
\newcommand{\Addr}{{\rm Addr}}
\newcommand{\Exc}{{\rm ExName}}
\newcommand{\BasVal}{{\rm BasVal}}
\newcommand{\SVal}{{\rm SVal}}
\newcommand{\BasExc}{{\rm BasExName}}
\newcommand{\BasTyp}{{\rm BasTyp}}
\newcommand{\CONT}{{\tt !}}
\newcommand{\ASS}{{\tt :=}}
\newcommand{\FAIL}{{\rm FAIL}}
\newcommand{\Fail}{{\rm FAIL}}
\newcommand{\fail}{{\rm FAIL}}
\newcommand{\APPLY}{{\rm APPLY}}

\newcommand{\A}{a}
\newcommand{\e}{\mbox{\it en}}
\newcommand{\sv}{\mbox{\it sv}}
\newcommand{\exval}{e}
\newcommand{\excs}{\mbox{\it ens}}
\newcommand{\exns}{\mbox{\it excons}} % used in the dynamic sem. of mod.
\newcommand{\f}{f}
\newcommand{\m}{m}
\newcommand{\mem}{\mbox{\it mem}}
\newcommand{\M}{M}
\newcommand{\n}{n}
\newcommand{\N}{N}
\newcommand{\p}{p}
%\newcommand{\r}{r}
\newcommand{\res}{\mbox{\it res}}
\newcommand{\s}{s}
\renewcommand{\t}{t}
\newcommand{\T}{T}
\newcommand{\U}{U}
\newcommand{\V}{v}
\newcommand{\vars}{\mbox{\it vars}}
\newcommand{\X}{X}

          % Compound Objects (Core Language)
\newcommand{\TyEnv}{{\rm TyEnv}}
\newcommand{\TE}{\mbox{$T\!E$}}
\newcommand{\TyStr}{{\rm TyStr}}

\newcommand{\ConEnv}{{\rm ConEnv}}
\newcommand{\CE}{\mbox{$C\!E$}}

\newcommand{\VarEnv}{{\rm VarEnv}}
\newcommand{\VE}{\mbox{$V\!E$}}

\newcommand{\ExnEnv}{{\rm ExConEnv}}
\newcommand{\EE}{\mbox{$E\!E$}}

\newcommand{\IntEnv}{{\rm IntEnv}}
\newcommand{\IE}{\mbox{$I\!E$}}

\newcommand{\Env}{{\rm Env}}
\newcommand{\E}{E}
%%%\newcommand{\longE}[1]{(\SE_{#1},\TE_{#1},\VE_{#1},\EE_{#1})}
\newcommand{\longE}[1]{(\SE_{#1},\TE_{#1},\VE_{#1})}

\newcommand{\StrEnv}{{\rm StrEnv}}
\newcommand{\SE}{\mbox{$S\!E$}}

\newcommand{\Str}{{\rm Str}}
\renewcommand{\S}{S}
%%%\newcommand{\longS}[1]{(\m_{#1},(\SE_{#1},\TE_{#1},\VE_{#1},\EE_{#1}))}
\newcommand{\longS}[1]{(\m_{#1},(\SE_{#1},\TE_{#1},\VE_{#1}))}

\newcommand{\Int}{{\rm Int}}
\newcommand{\I}{I}

\newcommand{\Context}{\rm Context}
\newcommand{\C}{C}


\newcommand{\Record}{{\rm Record}}
\newcommand{\ExVal}{{\rm ExVal}}
\newcommand{\Fun}{{\rm Fun}}  % used?
\newcommand{\Pack}{{\rm Pack}}
\newcommand{\Closure}{{\rm Closure}}
\newcommand{\FunctorClosure}{{\rm FunctorClosure}}
\newcommand{\Match}{{\rm Match}}
\newcommand{\State}{{\rm State}}
\newcommand{\StrExp}{{\rm StrExp}}
\newcommand{\Mem}{{\rm Mem}}
\newcommand{\ExcSet}{{\rm ExNameSet}}
\newcommand{\Val}{{\rm Val}}

\newcommand{\arity}{\mathop{\rm arity}\nolimits}
%\newcommand{\k}{\mbox{$k$}}
\newcommand{\longtauk}{(\tau_1,\cdots,\tau_k)}
\newcommand{\tauk}{\mbox{$\tau^{(k)}$}}
\newcommand{\longalphak}{(\alpha_1,\cdots,\alpha_k)}
\newcommand{\alphak}{\mbox{$\alpha^{(k)}$}}
\newcommand{\alphakt}{\mbox{$\alpha^{(k)}t$}}
%
\newcommand{\thetak}{\mbox{$\theta^{(k)}$}}
\newcommand{\tk}{\mbox{$\t^{(k)}$}}
\newcommand{\typefcn}{\theta}
\newcommand{\typefcnk}{\Lambda\alphak.\tau}
\newcommand{\Type}{{\rm Type}}
\newcommand{\ConsType}{{\rm ConsType}}
\newcommand{\RecType}{{\rm RecType}}
\newcommand{\FunType}{{\rm FunType}}
\newcommand{\constypek}{\t(\tau_1,\cdots,\tau_k)}
\newcommand{\TypeScheme}{{\rm TypeScheme}}
\newcommand{\tych}{\sigma}
\newcommand{\longtych}{\forall\alphak.\tau}
\newcommand{\Abs}{\mathop{\rm Abs_{\C}}\nolimits}
\newcommand{\Inter}{\mathop{\rm Inter}\nolimits}
\newcommand{\Rec}{\mathop{\rm Rec}\nolimits}
\newcommand{\TypeFcn}{{\rm TypeFcn}}
\newcommand{\TyConFcn}{\mathop{\rm TyCon}\nolimits} % used?
\newcommand{\TyVarFcn}{\mathop{\rm tyvars}\nolimits}
\newcommand{\imptyvars}{\mathop{\rm imptyvars}\nolimits}
\newcommand{\apptyvars}{\mathop{\rm apptyvars}\nolimits}
\newcommand{\scontype}{\mathop{\rm type}\nolimits}
\newcommand{\sconval}{\mathop{\rm val}\nolimits}
%
%         Compound Objects (Modules)
%
%
\newcommand{\Sig}{{\rm Sig}}
\newcommand{\sig}{\Sigma}
\newcommand{\longsig}[1]{(\N_{#1})\S_{#1}}
\newcommand{\FunSig}{{\rm FunSig}}
\newcommand{\funsig}{\Phi}
\newcommand{\longfunsig}[1]{(\N_{#1})(\S_{#1},(\N_{#1}')\S_{#1}
')}
\newcommand{\FunEnv}{{\rm FunEnv}}
\newcommand{\F}{F}

\newcommand{\SigEnv}{{\rm SigEnv}}
\newcommand{\G}{G}

\newcommand{\Basis}{{\rm Basis}}
\newcommand{\B}{B}
\newcommand{\Bstat}{B_{\rm STAT}}
\newcommand{\Bdyn}{B_{\rm DYN}}

\newcommand{\IntBasis}{{\rm IntBasis}}
\newcommand{\IB}{\mbox{$I\!B$}}


%         Selection of Components
%
\newcommand{\of}[2]{#1 \mathbin{\rm of} #2}
\newcommand{\In}{\mbox{\rm in}}
%
%         Names in Structures
\newcommand{\StrNamesFcn}{\mathop{\rm strnames}\nolimits}
\newcommand{\TyNamesFcn}{\mathop{\rm tynames}\nolimits}
\newcommand{\TyVarsFcn}{\mathop{\rm tyvars}\nolimits}
\newcommand{\NamesFcn}{\mathop{\rm names}\nolimits}
%
%         Type Schemes (assume math mode)
%
\newcommand{\cl}[2]{{\rm Clos}_{#1}#2}
%
%         Realisations (assume math mode)
%
\newcommand{\tyrea}{\varphi_{\rm Ty}}
\newcommand{\TyRea}{{\rm TyRea}}
\newcommand{\strrea}{\varphi_{\rm Str}}
\newcommand{\StrRea}{{\rm StrRea}}
\newcommand{\rea}{\varphi}
\newcommand{\longrea}{(\tyrea,\strrea)}
%
%             Support (assume math mode)
%
\newcommand{\Supp}{\mathop{\rm Supp}\nolimits}
\newcommand{\Yield}{\mathop{\rm Yield}\nolimits}
%
%           Instantiation (assume math mode)
%
\newcommand{\siginst}[3]{#1 {\geq_{#2}} #3}
\newcommand{\sigord}[3]{#1 {\geq_{#2}} #3}
\newcommand{\funsiginst}[3]{#1 {\geq_{#2}} #3}
%
%            Inference Rules
%
%
\newcommand{\ts}{\vdash}
\newcommand{\tsdyn}{\vdash_{\rm DYN}}
\newcommand{\tsstat}{\vdash_{\rm STAT}}

\newcommand{\ra}{\Rightarrow}

%            Initial Static Basis

%              Type names
\newcommand{\BOOL}{\mbox{\tt bool}}
\newcommand{\INT}{\mbox{\tt int}}
\newcommand{\REAL}{\mbox{\tt real}}
\newcommand{\NUM}{\mbox{\tt num}}
\newcommand{\EXCN}{\mbox{\tt exn}}
\newcommand{\STRING}{\mbox{\tt string}}
\newcommand{\LIST}{\mbox{\tt list}}
\newcommand{\INSTREAM}{\mbox{\tt instream}}
\newcommand{\OUTSTREAM}{\mbox{\tt outstream}}

%              Constructors
\newcommand{\FALSE}{\mbox{\tt false}}
\newcommand{\TRUE}{\mbox{\tt true}}
\newcommand{\NIL}{\mbox{\tt nil}}
\newcommand{\REF}{\mbox{\tt ref}}
\newcommand{\UNIT}{\mbox{\tt unit}}

%              Basic Values BasVal
%\newcommand{\MAP}{\mbox{\tt map}}
%\newcommand{\REV}{\mbox{\tt rev}}
\newcommand{\NOT}{\mbox{\tt not}}
%\newcommand{\NEG}{\mbox{\verb-~-}}
%\newcommand{\ABS}{\mbox{\tt abs}}
%\newcommand{\FLOOR}{\mbox{\tt floor}}
%\newcommand{\REAL}{\mbox{\tt real}}
%\newcommand{\SQRT}{\mbox{\tt sqrt}}
%\newcommand{\SIN}{\mbox{\tt sin}}
%\newcommand{\COS}{\mbox{\tt cos}}
%\newcommand{\ARCTAN}{\mbox{\tt arctan}}
%\newcommand{\EXP}{\mbox{\tt exp}}
%\newcommand{\LN}{\mbox{\tt ln}}
%\newcommand{\SIZE}{\mbox{\tt size}}
%\newcommand{\CHR}{\mbox{\tt chr}}
%\newcommand{\ORD}{\mbox{\tt ord}}
%\newcommand{\EXPLODE}{\mbox{\tt explode}}
%\newcommand{\IMPLODE}{\mbox{\tt implode}}
\newcommand{\REALDIV}{\mbox{\tt /}}
\newcommand{\DIV}{\mbox{\tt div}}
\newcommand{\MOD}{\mbox{\tt mod}}
\newcommand{\TIMES}{\mbox{\tt  *}}
\newcommand{\PLUS}{\mbox{\tt +}}
\newcommand{\MINUS}{\mbox{\tt -}}
\newcommand{\CONCAT}{\mbox{\tt\char`\^}}
%\newcommand{\APPEND}{\mbox{\verb-@-}}
%\newcommand{\EQ}{\mbox{\verb-=-}}
\newcommand{\NEQ}{\mbox{\verb-<>-}}
\newcommand{\LESS}{\mbox{\verb-<-}}
\newcommand{\GREATER}{\mbox{\verb->-}}
\newcommand{\LEQ}{\mbox{\verb-<=-}}
\newcommand{\GEQ}{\mbox{\verb->=-}}
%\newcommand{\COMP}{\mbox{\tt o}}

%\newcommand{\STDIN}{\mbox{\tt std\_in}}
%\newcommand{\OPENIN}{\mbox{\tt open\_in}}
%\newcommand{\INPUT}{\mbox{\tt input}}
%\newcommand{\LOOKAHEAD}{\mbox{\tt lookahead}}
%\newcommand{\CLOSEIN}{\mbox{\tt close\_in}}
%\newcommand{\ENDSTREAM}{\mbox{\tt end\_of\_stream}}
%\newcommand{\STDOUT}{\mbox{\tt std\_out}}
%\newcommand{\OPENOUT}{\mbox{\tt open\_out}}
%\newcommand{\OUTPUT}{\mbox{\tt output}}
%\newcommand{\CLOSEOUT}{\mbox{\tt close\_out}}
%\newcommand{\IOFAILURE}{\mbox{\tt io\_failure}}
\newcommand{\comment}{{\it Comment:\ }}
\newcommand{\comments}{{\it Comments:\ }}
\newcommand{\rulesec}[2]{\subsection*{{\bf#1}\hfill\fbox{$#2$}}}
%
%\font\msxm=msxm10
%\textfont10=\msxm
\mathchardef\restrict="0A16
%
% $$f\restrict_A$$                   % Example of use
%alignment
%\halign{\indent$#$&\quad$#$&\quad$#$\hfil&\quad\parbox[t]{6cm}{\strut#\strut}\cr
