# HG changeset patch
# User wenzelm
# Date 1512641575 -3600
# Node ID 39117b6f0b2ea030ec3a527f9be00e669911dd00
# Parent  8021ea06aad830800b2de5bd1af8ad53e3b5312a
obsolete (used to be part of old src/Pure/codegen.ML);

diff -r 8021ea06aad8 -r 39117b6f0b2e lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Wed Dec 06 21:43:20 2017 +0100
+++ b/lib/texinputs/isabellesym.sty	Thu Dec 07 11:12:55 2017 +0100
@@ -357,7 +357,6 @@
 \newcommand{\isasymdieresis}{\isatext{\"\relax}}
 \newcommand{\isasymcedilla}{\isatext{\c\relax}}
 \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
-\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
 \newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
 \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}