# HG changeset patch
# User wenzelm
# Date 771152985 -7200
# Node ID 7c7e71be40c89a8a277e15173712c335cdffa27c
# Parent  ab09293bccc7052e99460541dd444e819a83014b
added OldMixfix;

diff -r ab09293bccc7 -r 7c7e71be40c8 src/ZF/ex/Bin.ML
--- 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",
diff -r ab09293bccc7 -r 7c7e71be40c8 src/ZF/ex/Comb.ML
--- 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",
diff -r ab09293bccc7 -r 7c7e71be40c8 src/ZF/ex/Prop.ML
--- 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",