diff -r 3ca9d49fd662 -r 7b6d8b8d4580 src/ZF/ex/Bin.ML
--- a/src/ZF/ex/Bin.ML	Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Bin.ML	Fri Jul 01 11:04:12 1994 +0200
@@ -11,11 +11,9 @@
  (val thy = Univ.thy;
   val rec_specs = 
       [("bin", "univ(0)",
-	  [(["Plus", "Minus"],	"i"),
-	   (["op $$"],		"[i,i]=>i")])];
+	  [(["Plus", "Minus"],	"i", NoSyn),
+	   (["$$"],		"[i,i]=>i", Infixl 60)])];
   val rec_styp = "i";
-  val ext = Some (Syntax.simple_sext
-		  [OldMixfix.Infixl("$$", "[i,i] => i", 60)]);
   val sintrs = 
 	  ["Plus : bin",
 	   "Minus : bin",