# HG changeset patch # User wenzelm # Date 1527248878 -7200 # Node ID 77f6fa78b6e1610a03afeba9ce66cbade8166b80 # Parent 5ff0ccc7488458a8594bab289d812559c5763b71 proper output; diff -r 5ff0ccc74884 -r 77f6fa78b6e1 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Thu May 24 22:28:26 2018 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri May 25 13:47:58 2018 +0200 @@ -100,7 +100,7 @@ parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) - | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) + | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", quoted s, int p]) | pretty_mixfix (Binder (s, p1, p2, _)) = parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) | pretty_mixfix (Structure _) = parens [keyword "structure"];