diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean
index ca0a262326..88d40df871 100644
--- a/library/standard/tactic.lean
+++ b/library/standard/tactic.lean
@@ -20,7 +20,7 @@ definition and_then   (t1 t2 : tactic) : tactic := tactic_value
 definition or_else    (t1 t2 : tactic) : tactic := tactic_value
 definition repeat     (t : tactic) : tactic := tactic_value
 definition now        : tactic := tactic_value
-definition exact      : tactic := tactic_value
+definition assumption : tactic := tactic_value
 definition state      : tactic := tactic_value
 definition fail       : tactic := tactic_value
 definition id         : tactic := tactic_value
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index e96248b5ae..e815f33cb8 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -83,7 +83,7 @@ register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tact
 static name g_tac("tactic");
 static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); });
 static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); });
-static register_simple_tac reg_exact(name(g_tac, "exact"), []() { return assumption_tactic(); });
+static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { return assumption_tactic(); });
 static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); });
 static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); });
 static register_bin_tac reg_then(name(g_tac, "and_then"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean
index 69de80fa08..ac9f727e9c 100644
--- a/tests/lean/run/have5.lean
+++ b/tests/lean/run/have5.lean
@@ -5,8 +5,8 @@ axiom Ha : a
 axiom Hb : b
 axiom Hc : c
 print raw
-  have H1 : a, by exact,
-  then have H2 : b, by exact,
-  have H3 : c, by exact,
-  then have H4 : d, by exact,
+  have H1 : a, by assumption,
+  then have H2 : b, by assumption,
+  have H3 : c, by assumption,
+  then have H4 : d, by assumption,
   H4
\ No newline at end of file
diff --git a/tests/lean/run/t8.lean b/tests/lean/run/t8.lean
index 316343cbb8..e5c0240135 100644
--- a/tests/lean/run/t8.lean
+++ b/tests/lean/run/t8.lean
@@ -1,3 +1,3 @@
 import standard
 using tactic
-print raw (by exact)
\ No newline at end of file
+print raw (by assumption)
\ No newline at end of file
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index 09ed65769c..cf4729fa68 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -2,4 +2,4 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by exact
+:= by assumption
diff --git a/tests/lean/run/tactic2.lean b/tests/lean/run/tactic2.lean
index 1c66a94205..fd64eb64e1 100644
--- a/tests/lean/run/tactic2.lean
+++ b/tests/lean/run/tactic2.lean
@@ -2,6 +2,6 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by state; exact
+:= by state; assumption
 
 check tst
\ No newline at end of file
diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean
index 8137207f3c..dda820eddf 100644
--- a/tests/lean/run/tactic3.lean
+++ b/tests/lean/run/tactic3.lean
@@ -4,6 +4,6 @@ using tactic
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
 := by trace "first";  state; now  |
       trace "second"; state; fail |
-      trace "third";  exact
+      trace "third";  assumption
 
 check tst
\ No newline at end of file
diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean
index 43ae4be558..cda3ca0203 100644
--- a/tests/lean/run/tactic4.lean
+++ b/tests/lean/run/tactic4.lean
@@ -4,7 +4,7 @@ using tactic (renaming id->id_tac)
 definition id {A : Type} (a : A) := a
 
 definition simple {A : Bool} : tactic
-:= unfold @id.{1}; exact
+:= unfold @id.{1}; assumption
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
 := by simple
diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean
index ac9919fd76..b4b8f520c4 100644
--- a/tests/lean/run/tactic5.lean
+++ b/tests/lean/run/tactic5.lean
@@ -4,6 +4,6 @@ using tactic (renaming id->id_tac)
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by !(unfold @id; state); exact
+:= by !(unfold @id; state); assumption
 
 check tst
\ No newline at end of file
diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean
index 455dbb3e7d..e111ed4474 100644
--- a/tests/lean/run/tactic6.lean
+++ b/tests/lean/run/tactic6.lean
@@ -4,6 +4,6 @@ using tactic (renaming id->id_tac)
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by unfold id; exact
+:= by unfold id; assumption
 
 check tst
diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean
index fb21464743..c59864d5fb 100644
--- a/tests/lean/run/tactic7.lean
+++ b/tests/lean/run/tactic7.lean
@@ -2,11 +2,11 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by apply and_intro; state; exact; apply and_intro; !exact
+:= by apply and_intro; state; assumption; apply and_intro; !assumption
 check tst
 
 theorem tst2 {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by !((apply @and_intro | exact) ; trace "STEP"; state; trace "----------")
+:= by !((apply @and_intro | assumption) ; trace "STEP"; state; trace "----------")
 
 check tst2
 
diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean
index 4d2969139a..55d29d8166 100644
--- a/tests/lean/run/tactic9.lean
+++ b/tests/lean/run/tactic9.lean
@@ -2,5 +2,5 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : ((fun x : Bool, x) A) ∧ B ∧ A
-:= by apply and_intro; beta; exact; apply and_intro; !exact
+:= by apply and_intro; beta; assumption; apply and_intro; !assumption