more markup for syntax consts;
authorwenzelm
Fri, 23 Aug 2024 22:47:51 +0200
changeset 80753 66893c47500d
parent 80752 2c9b5288eb84
child 80754 701912f5645a
more markup for syntax consts;
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),