src/Pure/sign.ML
changeset 21183 a76f457b6d86
parent 20784 eece9aaaf352
child 21206 2af4c7b3f7ef
--- a/src/Pure/sign.ML	Sun Nov 05 21:44:35 2006 +0100
+++ b/src/Pure/sign.ML	Sun Nov 05 21:44:37 2006 +0100
@@ -114,6 +114,7 @@
   val declared_tyname: theory -> string -> bool
   val declared_const: theory -> string -> bool
   val const_monomorphic: theory -> string -> bool
+  val const_syntax_name: theory -> string -> string
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
   val class_space: theory -> NameSpace.T
@@ -289,6 +290,7 @@
 val the_const_type = Consts.declaration o consts_of;
 val const_type = try o the_const_type;
 val const_monomorphic = Consts.monomorphic o consts_of;
+val const_syntax_name = Consts.syntax_name o consts_of;
 val const_typargs = Consts.typargs o consts_of;
 val const_instance = Consts.instance o consts_of;