expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these;

--- a/lib/texinputs/isabelle.sty	Mon Jan 29 19:26:14 2018 +0100
+++ b/lib/texinputs/isabelle.sty	Mon Jan 29 20:37:28 2018 +0100
@@ -14,9 +14,9 @@
 \newcommand{\isastyleminor}{\UNDEF}
 \newcommand{\isastyleminortt}{\UNDEF}
 \newcommand{\isastylescript}{\UNDEF}
-\newcommand{\isastyletext}{\normalsize\rm}
-\newcommand{\isastyletxt}{\rm}
-\newcommand{\isastylecmt}{\rm}
+\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
+\newcommand{\isastyletxt}{\normalfont\rmfamily}
+\newcommand{\isastylecmt}{\normalfont\rmfamily}
 
 \newcommand{\isaspacing}{%
   \sfcode 42 1000 % .
@@ -120,12 +120,12 @@
 % keyword and section markup
 
 \newcommand{\isakeyword}[1]
-{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
+{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
 \newcommand{\isacommand}[1]{\isakeyword{#1}}
 
 \newcommand{\isakeywordcontrol}[1]
-{\emph{\bf\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
+{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
 
 \newcommand{\isamarkupheader}[1]{\section{#1}}
 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
@@ -149,30 +149,30 @@
 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
 
 \newcommand{\isabellestyledefault}{%
-\def\isastyle{\small\tt\slshape}%
-\def\isastylett{\small\tt}%
-\def\isastyleminor{\small\tt\slshape}%
-\def\isastyleminortt{\small\tt}%
-\def\isastylescript{\footnotesize\tt\slshape}%
+\def\isastyle{\small\normalfont\ttfamily\slshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
+\def\isastyleminortt{\small\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
 \isachardefaults%
 }
 \isabellestyledefault
 
 \newcommand{\isabellestylett}{%
-\def\isastyle{\small\tt}%
-\def\isastylett{\small\tt}%
-\def\isastyleminor{\small\tt}%
-\def\isastyleminortt{\small\tt}%
-\def\isastylescript{\footnotesize\tt}%
+\def\isastyle{\small\normalfont\ttfamily}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\small\normalfont\ttfamily}%
+\def\isastyleminortt{\small\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\ttfamily}%
 \isachardefaults%
 }
 
 \newcommand{\isabellestyleit}{%
-\def\isastyle{\small\it}%
-\def\isastylett{\small\tt}%
-\def\isastyleminor{\it}%
-\def\isastyleminortt{\tt}%
-\def\isastylescript{\footnotesize\it}%
+\def\isastyle{\small\normalfont\itshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\normalfont\itshape}%
+\def\isastyleminortt{\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\itshape}%
 \isachardefaults%
 \def\isacharunderscorekeyword{\mbox{-}}%
 \def\isacharbang{\isamath{!}}%
@@ -228,11 +228,11 @@
 
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
-\def\isastyle{\small\sl}%
-\def\isastylett{\small\tt}%
-\def\isastyleminor{\sl}%
-\def\isastyleminortt{\tt}%
-\def\isastylescript{\footnotesize\sl}%
+\def\isastyle{\small\normalfont\slshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\normalfont\slshape}%
+\def\isastyleminortt{\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\slshape}%
 }
 
 

--- a/lib/texinputs/isabellesym.sty	Mon Jan 29 19:26:14 2018 +0100
+++ b/lib/texinputs/isabellesym.sty	Mon Jan 29 20:37:28 2018 +0100
@@ -328,25 +328,25 @@
 \newcommand{\isasymnatural}{\isamath{\natural}}
 \newcommand{\isasymsharp}{\isamath{\sharp}}
 \newcommand{\isasymangle}{\isamath{\angle}}
-\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
-\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
+\newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}}
+\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}}
 \newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires textcomp
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires textcomp
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires textcomp
-\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
-\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
-\newcommand{\isasymsection}{\isatext{\rm\S}}
-\newcommand{\isasymparagraph}{\isatext{\rm\P}}
-\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
-\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
+\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}}  %requires textcomp
+\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}}  %requires textcomp
+\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}}  %requires textcomp
+\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}}
+\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}}
+\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}}
 \newcommand{\isasymeuro}{\isatext{\euro}}  %requires eurosym
 \newcommand{\isasympounds}{\isamath{\pounds}}
 \newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
 \newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
 \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires textcomp
-\newcommand{\isasymhyphen}{\isatext{\rm-}}
+\newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}}  %requires textcomp
+\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}}
 \newcommand{\isasymamalg}{\isamath{\amalg}}
 \newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
 \newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
@@ -362,7 +362,7 @@
 \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
 \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
 \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
-\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
+\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
 \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}