# HG changeset patch
# User paulson
# Date 835108024 -7200
# Node ID 23bda45846a2c72e5b1a35bf768f660ca8239ef3
# Parent  debfc40b7756fdbf28476c6ca4eed0289f6692e4
Translation infixes <->, etc., no longer available at top-level

diff -r debfc40b7756 -r 23bda45846a2 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Jun 18 16:20:30 1996 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Jun 18 16:27:04 1996 +0200
@@ -13,10 +13,6 @@
   include SYN_TRANS0
   include MIXFIX0
   include PRINTER0
-  datatype 'a trrule =
-    op |-> of 'a * 'a |
-    op <-| of 'a * 'a |
-    op <-> of 'a * 'a
   end;
 
 signature SYNTAX =