# HG changeset patch
# User wenzelm
# Date 1144529491 -7200
# Node ID f2446ce045901cdee43beddd97e4db1fb4ed3b38
# Parent  3ff5f1777743815c4c0478758da798245f889cec
removed fix_mixfix;
added const_mixfix, mixfix_const;

diff -r 3ff5f1777743 -r f2446ce04590 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sat Apr 08 22:51:30 2006 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sat Apr 08 22:51:31 2006 +0200
@@ -29,7 +29,8 @@
   val pretty_mixfix: mixfix -> Pretty.T
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
-  val fix_mixfix: string -> mixfix -> mixfix
+  val const_mixfix: string -> mixfix -> string * mixfix
+  val mixfix_const: string -> mixfix -> string * bool
   val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
   val mixfix_content: mixfix -> string list list
@@ -122,11 +123,16 @@
   | const_name c (Infixr _) = "op " ^ deprecated (strip_esc c)
   | const_name c _ = c;
 
-fun fix_mixfix c (Infix p) = (deprecated (strip_esc c); InfixName (c, p))
-  | fix_mixfix c (Infixl p) = (deprecated (strip_esc c); InfixlName (c, p))
-  | fix_mixfix c (Infixr p) = (deprecated (strip_esc c); InfixrName (c, p))
+fun fix_mixfix c (Infix p) = InfixName (c, p)
+  | fix_mixfix c (Infixl p) = InfixlName (c, p)
+  | fix_mixfix c (Infixr p) = InfixrName (c, p)
   | fix_mixfix _ mx = mx;
 
+fun const_mixfix c mx = (const_name c mx, fix_mixfix c mx);
+
+fun mixfix_const c NoSyn = (c, true)
+  | mixfix_const c _ = (Lexicon.constN ^ c, false);
+
 fun map_mixfix _ NoSyn = NoSyn
   | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
   | map_mixfix f (Delimfix sy) = Delimfix (f sy)