--- 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;