Removal of needless occurrences of "op"
authorpaulson
Mon, 02 Dec 1996 10:23:28 +0100
changeset 2287 94b70aeb7d1f
parent 2286 c2f76a5bad65
child 2288 16e7a5adb679
Removal of needless occurrences of "op"
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