Removal of needless occurrences of "op"
authorpaulson
Mon Dec 02 10:23:28 1996 +0100 (1996-12-02)
changeset 228794b70aeb7d1f
parent 2286 c2f76a5bad65
child 2288 16e7a5adb679
Removal of needless occurrences of "op"
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Dec 02 10:22:41 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Dec 02 10:23:28 1996 +0100
     1.3 @@ -25,9 +25,9 @@
     1.4    include MIXFIX1
     1.5    include PRINTER0
     1.6    datatype 'a trrule =
     1.7 -    op |-> of 'a * 'a |
     1.8 -    op <-| of 'a * 'a |
     1.9 -    op <-> of 'a * 'a
    1.10 +    |-> of 'a * 'a |
    1.11 +    <-| of 'a * 'a |
    1.12 +    <-> of 'a * 'a
    1.13    type syntax
    1.14    val extend_log_types: syntax -> string list -> syntax
    1.15    val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax