# HG changeset patch
# User wenzelm
# Date 1632080151 -7200
# Node ID 3360ea6b659dbb03eb7dce90b0bd052dc798199a
# Parent  0a4e93250e44b2a14f84ed6f2cd50e91c19909bd
more control symbols;

diff -r 0a4e93250e44 -r 3360ea6b659d etc/symbols
--- a/etc/symbols	Sun Sep 19 21:14:14 2021 +0200
+++ b/etc/symbols	Sun Sep 19 21:35:51 2021 +0200
@@ -491,7 +491,9 @@
 \<^oracle_name>         argument: cartouche
 \<^Const>               argument: cartouche
 \<^Const_>              argument: cartouche
+\<^Const_fn>            argument: cartouche
 \<^Type>                argument: cartouche
+\<^Type_fn>             argument: cartouche
 \<^code>                argument: cartouche
 \<^computation>         argument: cartouche
 \<^computation_conv>    argument: cartouche
diff -r 0a4e93250e44 -r 3360ea6b659d lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Sun Sep 19 21:14:14 2021 +0200
+++ b/lib/texinputs/isabellesym.sty	Sun Sep 19 21:35:51 2021 +0200
@@ -478,7 +478,9 @@
 \newcommand{\isactrlvar}{\isakeywordcontrol{var}}
 \newcommand{\isactrlConst}{\isakeywordcontrol{Const}}
 \newcommand{\isactrlConstUNDERSCORE}{\isakeywordcontrol{Const{\isacharunderscore}}}
+\newcommand{\isactrlConstUNDERSCOREfn}{\isakeywordcontrol{Const{\isacharunderscore}fn}}
 \newcommand{\isactrlType}{\isakeywordcontrol{Type}}
+\newcommand{\isactrlTypeUNDERSCOREfn}{\isakeywordcontrol{Type{\isacharunderscore}fn}}
 
 \newcommand{\isactrlcode}{\isakeywordcontrol{code}}
 \newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}