diff -r 7a9c559bc518 -r c8e08d8ffb93 etc/symbols
--- a/etc/symbols	Sat Mar 30 12:07:31 2019 +0100
+++ b/etc/symbols	Sat Mar 30 20:54:47 2019 +0100
@@ -408,6 +408,7 @@
 \<^named_theorems>      argument: cartouche
 \<^nonterminal>         argument: cartouche
 \<^path>                argument: cartouche
+\<^path_binding>        argument: cartouche
 \<^plugin>              argument: cartouche
 \<^print>
 \<^prop>                argument: cartouche