# HG changeset patch
# User wenzelm
# Date 1139534572 -3600
# Node ID 64ad6c5204648b24fbc89b3f1aeab7fe8136018d
# Parent  2fbb3d809026617f8ffe8a1d7c71d30abcaa9f20
added mixfix_conflict;

diff -r 2fbb3d809026 -r 64ad6c520464 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Feb 10 02:22:50 2006 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 10 02:22:52 2006 +0100
@@ -32,6 +32,7 @@
   val fix_mixfix: string -> mixfix -> mixfix
   val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
+  val mixfix_conflict: mixfix * mixfix -> bool
 end;
 
 signature MIXFIX =
@@ -142,6 +143,23 @@
   | mixfix_args (Binder _) = 1
   | mixfix_args Structure = 0;
 
+fun mixfix_conflict (mx1, mx2) =
+  let
+    fun content kind sy = SOME (kind, SynExt.mfix_delims sy);
+    fun content_of (Mixfix (sy, _, _)) = content 0 sy
+      | content_of (Delimfix sy) = content 0 sy
+      | content_of (InfixName (sy, _)) = content 1 sy
+      | content_of (InfixlName (sy, _)) = content 1 sy
+      | content_of (InfixrName (sy, _)) = content 1 sy
+      | content_of (Binder (sy, _, _)) = content 2 sy
+      | content_of _ = NONE;
+  in
+    (case (content_of mx1, content_of mx2) of
+      (SOME (kind1, delims1), SOME (kind2, delims2)) =>
+        (kind1 = 0 orelse kind2 = 0 orelse kind1 = kind2) andalso delims1 = delims2
+    | _ => false)
+  end;
+
 
 (* syn_ext_types *)