removed mixfix_content;
authorwenzelm
Fri, 29 Sep 2006 22:47:04 +0200
changeset 20786 96077403f619
parent 20785 d60f81c56fd4
child 20787 406d990006af
removed mixfix_content;
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;