--- a/src/ZF/ex/bin.ML Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/bin.ML Thu Sep 30 10:54:01 1993 +0100
@@ -14,18 +14,7 @@
[(["Plus", "Minus"], "i"),
(["op $$"], "[i,i]=>i")])];
val rec_styp = "i";
- val ext = Some (NewSext {
- mixfix =
- [Infixl("$$", "[i,i] => i", 60)],
- xrules = [],
- parse_ast_translation = [],
- parse_preproc = None,
- parse_postproc = None,
- parse_translation = [],
- print_translation = [],
- print_preproc = None,
- print_postproc = None,
- print_ast_translation = []});
+ val ext = Some (Syntax.simple_sext [Infixl("$$", "[i,i] => i", 60)]);
val sintrs =
["Plus : bin",
"Minus : bin",