# HG changeset patch
# User wenzelm
# Date 1159562824 -7200
# Node ID 96077403f619acad26a834a69f19c612a99d5d67
# Parent  d60f81c56fd490bbf5ee1f32a4fdb0297a21f24f
removed mixfix_content;

diff -r d60f81c56fd4 -r 96077403f619 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Sep 29 22:47:03 2006 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Sep 29 22:47:04 2006 +0200
@@ -32,7 +32,6 @@
   val const_mixfix: string -> mixfix -> string * mixfix
   val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
-  val mixfix_content: mixfix -> string list list
 end;
 
 signature MIXFIX =
@@ -232,19 +231,4 @@
       mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
   end;
 
-fun mixfix_content mx =
-  let
-    fun delims sy = SynExt.mfix_delims sy;
-    fun op_delims sy = let val ds = delims sy in ["op" :: ds, ds] end;
-  in
-    case mx of
-      Mixfix (sy, _, _) => [delims sy]
-    | Delimfix sy => [delims sy]
-    | InfixName (sy, _) => op_delims sy
-    | InfixlName (sy, _) => op_delims sy
-    | InfixrName (sy, _) => op_delims sy
-    | Binder (sy, _, _) => [delims sy @ ["."]]
-    | _ => []
-  end;
-
 end;