# HG changeset patch
# User wenzelm
# Date 1162759477 -3600
# Node ID a76f457b6d86b184d741ebcd5b40de3cda25e7a8
# Parent  747ff99b35eed410c077d16d0e2a2757fdb3a823
added const_syntax_name;

diff -r 747ff99b35ee -r a76f457b6d86 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Nov 05 21:44:35 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 05 21:44:37 2006 +0100
@@ -13,6 +13,7 @@
   val init: theory -> Proof.context
   val full_name: Proof.context -> bstring -> string
   val consts_of: Proof.context -> Consts.T
+  val const_syntax_name: Proof.context -> string -> string
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val fact_index_of: Proof.context -> FactIndex.T
@@ -225,6 +226,7 @@
 val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
 
 val consts_of = #2 o #consts o rep_context;
+val const_syntax_name = Consts.syntax_name o consts_of;
 
 val thms_of = #thms o rep_context;
 val fact_index_of = #2 o thms_of;
diff -r 747ff99b35ee -r a76f457b6d86 src/Pure/sign.ML
--- 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;