--- a/src/ZF/ex/Bin.ML Thu Jun 09 11:02:14 1994 +0200
+++ b/src/ZF/ex/Bin.ML Thu Jun 09 11:09:45 1994 +0200
@@ -14,7 +14,7 @@
[(["Plus", "Minus"], "i"),
(["op $$"], "[i,i]=>i")])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext [Infixl("$$", "[i,i] => i", 60)]);
+ val ext = Some (Syntax.simple_sext [OldMixfix.Infixl("$$", "[i,i] => i", 60)]);
val sintrs =
["Plus : bin",
"Minus : bin",
--- a/src/ZF/ex/Comb.ML Thu Jun 09 11:02:14 1994 +0200
+++ b/src/ZF/ex/Comb.ML Thu Jun 09 11:09:45 1994 +0200
@@ -19,7 +19,7 @@
[(["K","S"], "i"),
(["op #"], "[i,i]=>i")])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext [Infixl("#", "[i,i] => i", 90)]);
+ val ext = Some (Syntax.simple_sext [OldMixfix.Infixl("#", "[i,i] => i", 90)]);
val sintrs =
["K : comb",
"S : comb",
--- a/src/ZF/ex/Prop.ML Thu Jun 09 11:02:14 1994 +0200
+++ b/src/ZF/ex/Prop.ML Thu Jun 09 11:09:45 1994 +0200
@@ -17,8 +17,8 @@
(["op =>"], "[i,i]=>i")])];
val rec_styp = "i";
val ext = Some (Syntax.simple_sext
- [Mixfix("#_", "i => i", "Var", [100], 100),
- Infixr("=>", "[i,i] => i", 90)]);
+ [OldMixfix.Mixfix("#_", "i => i", "Var", [100], 100),
+ OldMixfix.Infixr("=>", "[i,i] => i", 90)]);
val sintrs =
["Fls : prop",
"n: nat ==> #n : prop",