diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 163fbab2f6..0528611593 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -906,7 +906,7 @@ tactic.done
 private meta def show_goal_aux (p : pexpr) : list expr → list expr → tactic unit
 | []      r := fail "show_goal tactic failed"
 | (g::gs) r := do
-  do {set_goals [g], g_ty ← target, ty ← i_to_expr p, unify g_ty ty >> set_goals (g :: r.reverse ++ gs) }
+  do {set_goals [g], g_ty ← target, ty ← i_to_expr p, unify g_ty ty, set_goals (g :: r.reverse ++ gs), tactic.change ty}
   <|>
   show_goal_aux gs (g::r)