diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 7e599b7b06..0e80a70ca7 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -50,8 +50,8 @@ do s ← read,
 meta_definition trace (s : string) : tactic unit :=
 return (_root_.trace s (λ u, ()))
 
-meta_definition trace_fmt (fmt : format) : tactic unit :=
-return (_root_.trace_fmt fmt (λ u, ()))
+meta_definition trace_fmt {A : Type} [has_to_format A] (a : A) : tactic unit :=
+return (_root_.trace_fmt (to_fmt a) (λ u, ()))
 
 /- Trace expression with respect to the main goal -/
 meta_definition trace_expr (e : expr) : tactic unit :=
diff --git a/tests/lean/run/fun_info1.lean b/tests/lean/run/fun_info1.lean
index c1ba83f9b6..b5bdb0244d 100644
--- a/tests/lean/run/fun_info1.lean
+++ b/tests/lean/run/fun_info1.lean
@@ -3,9 +3,9 @@ open tactic
 example (a : nat) : true :=
 by do
   trace "ite information:",
-  mk_const "ite" >>= get_fun_info >>= trace_fmt ∘ to_fmt,
+  mk_const "ite" >>= get_fun_info >>= trace_fmt,
   trace "eq.rec information:",
-  mk_const ("eq" <.> "rec") >>= get_fun_info >>= trace_fmt ∘ to_fmt,
+  mk_const ("eq" <.> "rec") >>= get_fun_info >>= trace_fmt,
   trace "and.intro information:",
-  mk_const ("and" <.> "intro") >>= get_fun_info >>= trace_fmt ∘ to_fmt,
+  mk_const ("and" <.> "intro") >>= get_fun_info >>= trace_fmt,
   mk_const "trivial" >>= exact
diff --git a/tests/lean/run/meta_tac6.lean b/tests/lean/run/meta_tac6.lean
index 7a07fd1417..fa53cb92a6 100644
--- a/tests/lean/run/meta_tac6.lean
+++ b/tests/lean/run/meta_tac6.lean
@@ -14,7 +14,7 @@ by do
       do t ← infer_type e,
          fmt₁ ← format_expr e,
          fmt₂ ← format_expr t,
-         trace_fmt (fmt₁ + to_fmt " : " + fmt₂)),
+         trace_fmt $ fmt₁ + to_fmt " : " + fmt₂),
     trace "----------",
     trace ("num: " + to_string n),
     trace_state,