# HG changeset patch
# User wenzelm
# Date 1724446071 -7200
# Node ID 66893c47500db4d4158f213b88726424f4984beb
# Parent  2c9b5288eb84122c4a029ea8980512a6a713d29a
more markup for syntax consts;

diff -r 2c9b5288eb84 -r 66893c47500d src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Aug 23 22:45:18 2024 +0200
+++ b/src/Pure/pure_thy.ML	Fri Aug 23 22:47:51 2024 +0200
@@ -220,6 +220,8 @@
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
+  #> Sign.syntax_deps
+   [("_bracket", ["\<^type>fun"]), ("_bigimpl", ["\<^const>Pure.imp"])]
   #> Sign.add_consts
    [(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn),
     (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn),