# HG changeset patch
# User wenzelm
# Date 1147807985 -7200
# Node ID 25eaa3660123d0c2975fc31ee8b58d90ceb20084
# Parent  09be06943252a2b2d1f5b1775cb6fff29aa7ec7a
added syntax interface;

diff -r 09be06943252 -r 25eaa3660123 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue May 16 21:33:01 2006 +0200
+++ b/src/Pure/consts.ML	Tue May 16 21:33:05 2006 +0200
@@ -21,6 +21,7 @@
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_early: T -> string -> xstring
+  val syntax: T -> string * mixfix -> string * typ * mixfix
   val read_const: T -> string -> term
   val certify: Pretty.pp -> Type.tsig -> T -> term -> term          (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
@@ -104,7 +105,7 @@
   | NONE => #1 (#1 (the_const consts c)));
 
 
-(* name space *)
+(* name space and syntax *)
 
 fun space_of (Consts ({decls = (space, _), ...}, _)) = space;
 
@@ -116,6 +117,12 @@
     SOME (_, false) => Syntax.constN ^ c
   | _ => extern consts c);
 
+fun syntax consts (c, mx) =
+  let
+    val ((T, _), early) = the_const consts c handle TYPE (msg, _, _) => error msg;
+    val c' = if early then NameSpace.base c else #1 (Syntax.mixfix_const c mx);
+  in (c', T, mx) end;
+
 
 (* read_const *)