# HG changeset patch
# User paulson
# Date 849518608 -3600
# Node ID 94b70aeb7d1fb2e9573c74dd694ead5b995b95c0
# Parent  c2f76a5bad65324f1cd2c783a4ee8e8a77686822
Removal of needless occurrences of "op"

diff -r c2f76a5bad65 -r 94b70aeb7d1f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Dec 02 10:22:41 1996 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Dec 02 10:23:28 1996 +0100
@@ -25,9 +25,9 @@
   include MIXFIX1
   include PRINTER0
   datatype 'a trrule =
-    op |-> of 'a * 'a |
-    op <-| of 'a * 'a |
-    op <-> of 'a * 'a
+    |-> of 'a * 'a |
+    <-| of 'a * 'a |
+    <-> of 'a * 'a
   type syntax
   val extend_log_types: syntax -> string list -> syntax
   val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax