diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 9f717ae2c3..57d85ef5c9 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -133,6 +133,6 @@ new_frontend namespace Lean --- macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData)) +macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData)) end Lean