src/Pure/Syntax/syntax.ML
changeset 2287 94b70aeb7d1f
parent 2202 cc15a7bfbe12
child 2366 a163d2be1bb5
--- 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