etc/symbols

--- a/etc/symbols	Tue Sep 21 12:35:38 2021 +0200
+++ b/etc/symbols	Tue Sep 21 13:12:14 2021 +0200
@@ -456,6 +456,8 @@
 \<^ctyp>                argument: cartouche
 \<^keyword>             argument: cartouche
 \<^locale>              argument: cartouche
+\<^make_judgment>
+\<^dest_judgment>
 \<^make_string>
 \<^method>              argument: cartouche
 \<^named_theorems>      argument: cartouche