diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 39b87b606f..1580b82e63 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -495,8 +495,8 @@ definition weak_order_dual {A : Type} (wo : weak_order A) : weak_order A :=
 ⦃ weak_order,
   le := λx y, y ≤ x,
   le_refl := le.refl,
-  le_trans := take a b c `b ≤ a` `c ≤ b`, le.trans `c ≤ b` `b ≤ a`,
-  le_antisymm := take a b `b ≤ a` `a ≤ b`, le.antisymm `a ≤ b` `b ≤ a` ⦄
+  le_trans := sorry, -- take a b c `b ≤ a` `c ≤ b`, le.trans `c ≤ b` `b ≤ a`,
+  le_antisymm := sorry ⦄ -- take a b `b ≤ a` `a ≤ b`, le.antisymm `a ≤ b` `b ≤ a` ⦄
 
 lemma le_dual_eq_le {A : Type} (wo : weak_order A) (a b : A) :
   @le _ (@weak_order.to_has_le _ (weak_order_dual wo)) a b =
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 0d02cc08ef..1b33f811fe 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -31,9 +31,9 @@ definition map (f : A → B) : list A → list B
 | []       := []
 | (a :: l) := f a :: map l
 
-theorem map_nil (f : A → B) : map f [] = []
+theorem map_nil (f : A → B) : map f [] = [] := rfl
 
-theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l
+theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l := rfl
 
 lemma map_concat (f : A → B) (a : A) : Πl, map f (concat a l) = concat (f a) (map f l)
 | nil    := rfl
@@ -140,7 +140,7 @@ definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
 | []     := []
 | (a::l) := if p a then a :: filter l else filter l
 
-theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = []
+theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = [] := rfl
 
 theorem filter_cons_of_pos [simp] {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, p a → filter p (a::l) = a :: filter p l :=
 λ l pa, if_pos pa
@@ -206,17 +206,17 @@ definition foldl (f : A → B → A) : A → list B → A
 | a []       := a
 | a (b :: l) := foldl (f a b) l
 
-theorem foldl_nil [simp] (f : A → B → A) (a : A) : foldl f a [] = a
+theorem foldl_nil [simp] (f : A → B → A) (a : A) : foldl f a [] = a := rfl
 
-theorem foldl_cons [simp] (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l
+theorem foldl_cons [simp] (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l := rfl
 
 definition foldr (f : A → B → B) : B → list A → B
 | b []       := b
 | b (a :: l) := f a (foldr b l)
 
-theorem foldr_nil [simp] (f : A → B → B) (b : B) : foldr f b [] = b
+theorem foldr_nil [simp] (f : A → B → B) (b : B) : foldr f b [] = b := rfl
 
-theorem foldr_cons [simp] (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l)
+theorem foldr_cons [simp] (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l) := rfl
 
 section foldl_eq_foldr
   -- foldl and foldr coincide when f is commutative and associative
@@ -269,11 +269,11 @@ foldr (λ a r, p a ∧ r) true l
 definition any (l : list A) (p : A → Prop) : Prop :=
 foldr (λ a r, p a ∨ r) false l
 
-theorem all_nil_eq [simp] (p : A → Prop) : all [] p = true
+theorem all_nil_eq [simp] (p : A → Prop) : all [] p = true := rfl
 
 theorem all_nil (p : A → Prop) : all [] p := trivial
 
-theorem all_cons_eq (p : A → Prop) (a : A) (l : list A) : all (a::l) p = (p a ∧ all l p)
+theorem all_cons_eq (p : A → Prop) (a : A) (l : list A) : all (a::l) p = (p a ∧ all l p) := rfl
 
 theorem all_cons {p : A → Prop} {a : A} {l : list A} (H1 : p a) (H2 : all l p) : all (a::l) p :=
 and.intro H1 H2
@@ -290,9 +290,9 @@ assume pa alllp, and.intro pa alllp
 theorem all_implies {p q : A → Prop} : ∀ {l}, all l p → (∀ x, p x → q x) → all l q
 | []     h₁ h₂ := trivial
 | (a::l) h₁ h₂ :=
-  have all l q, from all_implies (all_of_all_cons h₁) h₂,
+  have h₃ : all l q, from all_implies (all_of_all_cons h₁) h₂,
   have q a, from h₂ a (of_all_cons h₁),
-  all_cons_of_all this `all l q`
+  all_cons_of_all this h₃
 
 theorem of_mem_of_all {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → all l p → p a
 := sorry
@@ -312,9 +312,9 @@ theorem all_of_forall {p : A → Prop} : ∀ {l}, (∀a, a ∈ l → p a) → al
 | (a::l) H := all_cons (H a !mem_cons)
                        (all_of_forall (λ a' H', H a' (mem_cons_of_mem _ H')))
 
-theorem any_nil [simp] (p : A → Prop) : any [] p = false
+theorem any_nil [simp] (p : A → Prop) : any [] p = false := rfl
 
-theorem any_cons [simp] (p : A → Prop) (a : A) (l : list A) : any (a::l) p = (p a ∨ any l p)
+theorem any_cons [simp] (p : A → Prop) (a : A) (l : list A) : any (a::l) p = (p a ∨ any l p) := rfl
 
 theorem any_of_mem {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → p a → any l p
 := sorry
@@ -374,7 +374,7 @@ definition unzip : list (A × B) → list A × list B
   | (la, lb) := (a :: la, b :: lb)
   end
 
-theorem unzip_nil [simp] : unzip (@nil (A × B)) = ([], [])
+theorem unzip_nil [simp] : unzip (@nil (A × B)) = ([], []) := rfl
 
 theorem unzip_cons [simp] (a : A) (b : B) (l : list (A × B)) :
    unzip ((a, b) :: l) = match unzip l with (la, lb) := (a :: la, b :: lb) end :=
@@ -461,10 +461,10 @@ definition product : list A → list B → list (A × B)
 | []      l₂ := []
 | (a::l₁) l₂ := map (λ b, (a, b)) l₂ ++ product l₁ l₂
 
-theorem nil_product (l : list B) : product (@nil A) l = []
+theorem nil_product (l : list B) : product (@nil A) l = [] := rfl
 
 theorem product_cons (a : A) (l₁ : list A) (l₂ : list B)
-        : product (a::l₁) l₂ = map (λ b, (a, b)) l₂ ++ product l₁ l₂
+        : product (a::l₁) l₂ = map (λ b, (a, b)) l₂ ++ product l₁ l₂ := rfl
 
 theorem product_nil : ∀ (l : list A), product l (@nil B) = []
 | []     := rfl
diff --git a/library/data/list/set.lean b/library/data/list/set.lean
index 8404532eae..ee2e5e737f 100644
--- a/library/data/list/set.lean
+++ b/library/data/list/set.lean
@@ -360,7 +360,7 @@ definition erase_dup [decidable_eq A] : list A → list A
 | []        :=  []
 | (x :: xs) :=  if x ∈ xs then erase_dup xs else x :: erase_dup xs
 
-theorem erase_dup_nil [decidable_eq A] : erase_dup [] = ([] : list A)
+theorem erase_dup_nil [decidable_eq A] : erase_dup [] = ([] : list A) := rfl
 
 theorem erase_dup_cons_of_mem [decidable_eq A] {a : A} {l : list A} : a ∈ l → erase_dup (a::l) = erase_dup l :=
 assume ainl, calc
@@ -507,9 +507,9 @@ definition upto : nat → list nat
 | 0     := []
 | (n+1) := n :: upto n
 
-theorem upto_nil  : upto 0 = nil
+theorem upto_nil  : upto 0 = nil := rfl
 
-theorem upto_succ (n : nat) : upto (succ n) = n :: upto n
+theorem upto_succ (n : nat) : upto (succ n) = n :: upto n := rfl
 
 theorem length_upto : ∀ n, length (upto n) = n
 := sorry
@@ -575,7 +575,7 @@ definition union : list A → list A → list A
 | []      l₂ := l₂
 | (a::l₁) l₂ := if a ∈ l₂ then union l₁ l₂ else a :: union l₁ l₂
 
-theorem nil_union (l : list A) : union [] l = l
+theorem nil_union (l : list A) : union [] l = l := rfl
 
 theorem union_cons_of_mem {a : A} {l₂} : ∀ (l₁), a ∈ l₂ → union (a::l₁) l₂ = union l₁ l₂ :=
 take l₁, assume ainl₂, calc
@@ -806,7 +806,7 @@ definition inter : list A → list A → list A
 | []      l₂ := []
 | (a::l₁) l₂ := if a ∈ l₂ then a :: inter l₁ l₂ else inter l₁ l₂
 
-theorem inter_nil (l : list A) : inter [] l = []
+theorem inter_nil (l : list A) : inter [] l = [] := rfl
 
 theorem inter_cons_of_mem {a : A} (l₁ : list A) {l₂} : a ∈ l₂ → inter (a::l₁) l₂ = a :: inter l₁ l₂ :=
 assume i, if_pos i
diff --git a/library/data/list/sort.lean b/library/data/list/sort.lean
index 091ec2c038..55fabd82bb 100644
--- a/library/data/list/sort.lean
+++ b/library/data/list/sort.lean
@@ -193,7 +193,7 @@ lemma strongly_sorted_sort_aux : ∀ {n : nat} {l : list A} (h : length l = n),
       suppose x ∈ sort_aux R n (erase m l) leq,
       have x ∈ erase m l, from mem_perm (sort_aux_perm R leq) this,
       have x ∈ l,         from mem_of_mem_erase this,
-      show R m x,         from of_mem_of_all this `all l (R m)`),
+      show R m x,         from of_mem_of_all this sorry), -- `all l (R m)`),
   strongly_sorted.step hall ss
 
 variable {R}
diff --git a/library/data/list/sorted.lean b/library/data/list/sorted.lean
index 879e9cba29..fe50e53e24 100644
--- a/library/data/list/sorted.lean
+++ b/library/data/list/sorted.lean
@@ -33,10 +33,10 @@ sorry -- begin intros a l h, cases h, split, repeat assumption end
 lemma sorted.rect_on {P : list A → Type} : ∀ {l}, sorted R l → P [] → (∀ a l, sorted R l → P l → hd_rel R a l → P (a::l)) → P l
 | []     s h₁ h₂ := h₁
 | (a::l) s h₁ h₂ :=
-  have hd_rel R a l, from and.left (sorted_inv s),
-  have sorted R l,   from and.right (sorted_inv s),
-  have P l,          from sorted.rect_on this h₁ h₂,
-  h₂ a l `sorted R l` `P l` `hd_rel R a l`
+  have aux₁ : hd_rel R a l, from and.left (sorted_inv s),
+  have aux₂ : sorted R l,   from and.right (sorted_inv s),
+  have aux₃ : P l,          from sorted.rect_on aux₂ h₁ h₂,
+  h₂ a l aux₂ aux₃ aux₁
 
 lemma sorted_singleton (a : A) : sorted R [a] :=
 sorted.step !hd_rel.base !sorted.base
@@ -70,9 +70,9 @@ lemma sorted_of_strongly_sorted : ∀ {l}, strongly_sorted R l → sorted R l
 | []        h := !sorted.base
 | [a]       h := !sorted_singleton
 | (a::b::l) (strongly_sorted.step h₁ h₂) :=
-  have hd_rel R a (b::l), from hd_rel.step _ (of_all_cons h₁),
+  have aux : hd_rel R a (b::l), from hd_rel.step _ (of_all_cons h₁),
   have sorted R (b::l),   from sorted_of_strongly_sorted h₂,
-  sorted.step `hd_rel R a (b::l)` `sorted R (b::l)`
+  sorted.step aux this
 
 lemma sorted_extends (trans : transitive R) : ∀ {a l}, sorted R (a::l) → all l (R a)
 := sorry
@@ -94,9 +94,9 @@ theorem strongly_sorted_of_sorted_of_transitive (trans : transitive R) : ∀ {l}
 | []     h := !strongly_sorted.base
 | (a::l) h :=
   have sorted R l,          from and.right (sorted_inv h),
-  have strongly_sorted R l, from strongly_sorted_of_sorted_of_transitive this,
+  have aux : strongly_sorted R l, from strongly_sorted_of_sorted_of_transitive this,
   have all l (R a),         from sorted_extends trans h,
-  strongly_sorted.step `all l (R a)` `strongly_sorted R l`
+  strongly_sorted.step this aux
 
 open perm
 
diff --git a/library/data/nat/find.lean b/library/data/nat/find.lean
index 9de4c500bf..20f0b2ec71 100644
--- a/library/data/nat/find.lean
+++ b/library/data/nat/find.lean
@@ -100,9 +100,9 @@ match x with
 | 0 := λ f l0, by_cases
   (λ p0 : p 0,    tag 0 p0)
   (suppose ¬ p 0,
-    have lbp 1, from lbp_succ l0 this,
-    have 1 ≺ 0, from and.intro (lt.base 0) `lbp 1`,
-    f 1 `1 ≺ 0` `lbp 1`)
+    have h₁ : lbp 1, from lbp_succ l0 this,
+    have 1 ≺ 0, from and.intro (lt.base 0) h₁,
+    f 1 this h₁)
 | (succ n) := λ f lsn, by_cases
   (suppose p (succ n), tag (succ n) this)
   (suppose ¬ p (succ n),
diff --git a/library/data/num.lean b/library/data/num.lean
index aebbb735b6..b269de44d6 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -10,9 +10,9 @@ namespace pos_num
   theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff :=
   pos_num.induction_on a rfl (take n iH, rfl) (take n iH, rfl)
 
-  theorem succ_one                : succ one = bit0 one
-  theorem succ_bit1 (a : pos_num) : succ (bit1 a) = bit0 (succ a)
-  theorem succ_bit0 (a : pos_num) : succ (bit0 a) = bit1 a
+  theorem succ_one                : succ one = bit0 one := rfl
+  theorem succ_bit1 (a : pos_num) : succ (bit1 a) = bit0 (succ a) := rfl
+  theorem succ_bit0 (a : pos_num) : succ (bit0 a) = bit1 a := rfl
 
   theorem ne_of_bit0_ne_bit0 {a b : pos_num} (H₁ : bit0 a ≠ bit0 b) : a ≠ b :=
   suppose a = b,
@@ -35,16 +35,16 @@ namespace pos_num
   section
   variables (a b : pos_num)
 
-  theorem one_add_one     : one + one = bit0 one
-  theorem one_add_bit0    : one + (bit0 a) = bit1 a
-  theorem one_add_bit1    : one + (bit1 a) = succ (bit1 a)
-  theorem bit0_add_one    : (bit0 a) + one = bit1 a
-  theorem bit1_add_one    : (bit1 a) + one = succ (bit1 a)
-  theorem bit0_add_bit0   : (bit0 a) + (bit0 b) = bit0 (a + b)
-  theorem bit0_add_bit1   : (bit0 a) + (bit1 b) = bit1 (a + b)
-  theorem bit1_add_bit0   : (bit1 a) + (bit0 b) = bit1 (a + b)
-  theorem bit1_add_bit1   : (bit1 a) + (bit1 b) = succ (bit1 (a + b))
-  theorem one_mul         : one * a = a
+  theorem one_add_one     : one + one = bit0 one := rfl
+  theorem one_add_bit0    : one + (bit0 a) = bit1 a := rfl
+  theorem one_add_bit1    : one + (bit1 a) = succ (bit1 a) := rfl
+  theorem bit0_add_one    : (bit0 a) + one = bit1 a := rfl
+  theorem bit1_add_one    : (bit1 a) + one = succ (bit1 a) := rfl
+  theorem bit0_add_bit0   : (bit0 a) + (bit0 b) = bit0 (a + b) := rfl
+  theorem bit0_add_bit1   : (bit0 a) + (bit1 b) = bit1 (a + b) := rfl
+  theorem bit1_add_bit0   : (bit1 a) + (bit0 b) = bit1 (a + b) := rfl
+  theorem bit1_add_bit1   : (bit1 a) + (bit1 b) = succ (bit1 (a + b)) := rfl
+  theorem one_mul         : one * a = a := rfl
   end
 
   theorem mul_one         : ∀ a, a * one = a
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index 3e0df32247..6fad9f50fd 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -104,6 +104,7 @@ definition with_options_tac (o : expr) (t : tactic) : tactic := builtin
 -- with_options_tac is just a marker for the builtin 'with_attributes' notation
 definition with_attributes_tac (o : expr) (n : identifier_list) (t : tactic) : tactic := builtin
 
+/-
 definition simp          : tactic := #tactic with_options [blast.strategy "simp"] blast
 definition simp_nohyps   : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
 definition simp_topdown  : tactic := #tactic with_options [blast.strategy "simp", simplify.top_down true] blast
@@ -112,6 +113,7 @@ definition rec_simp      : tactic := #tactic with_options [blast.strategy "rec_s
 definition rec_inst_simp : tactic := #tactic with_options [blast.strategy "rec_ematch_simp"] blast
 definition grind         : tactic := #tactic with_options [blast.strategy "grind"] blast
 definition grind_simp    : tactic := #tactic with_options [blast.strategy "grind_simp"] blast
+-/
 
 definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
 
@@ -151,11 +153,11 @@ definition try         (t : tactic) : tactic := or_else t id
 definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
-definition trivial                  : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
+-- definition trivial                  : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
 definition do (n : num) (t : tactic) : tactic :=
 nat.rec id (λn t', and_then t t') (nat.of_num n)
 end tactic
-tactic_infixl `;`:15 := tactic.and_then
-tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
+-- tactic_infixl `;`:15 := tactic.and_then
+-- tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
 tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
 --tactic_notation `replace` s `with` t := tactic.replace_tac s t
diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean
index 0a1bf7fcc3..079497a20f 100644
--- a/library/tools/helper_tactics.lean
+++ b/library/tools/helper_tactics.lean
@@ -12,6 +12,6 @@ import logic.eq
 open tactic
 
 namespace helper_tactics
-  definition apply_refl := apply eq.refl
-  tactic_hint apply_refl
+  -- definition apply_refl := apply eq.refl
+  -- tactic_hint apply_refl
 end helper_tactics
diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 7906a678e9..4e10afba60 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -3,15 +3,19 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
 parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmd.cpp dependencies.cpp
-begin_end_annotation.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
+pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
-coercion_elaborator.cpp info_tactic.cpp
+coercion_elaborator.cpp
 init_module.cpp
-parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
 type_util.cpp elaborator_exception.cpp local_ref_info.cpp
 obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp
-parse_with_options_tactic.cpp opt_cmd.cpp prenum.cpp
-parse_with_attributes_tactic.cpp print_cmd.cpp elaborator_context.cpp elaborator.cpp
+opt_cmd.cpp prenum.cpp
+print_cmd.cpp elaborator_context.cpp elaborator.cpp
 # LEGACY
 old_elaborator.cpp
+# begin_end_annotation.cpp tactic_hint.cpp
+# info_tactic.cpp
+# parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
+# parse_with_options_tactic.cpp
+#parse_with_attributes_tactic.cpp
 )
diff --git a/src/frontends/lean/begin_end_annotation.cpp b/src/frontends/lean/begin_end_annotation.cpp
deleted file mode 100644
index 81ae4dd766..0000000000
--- a/src/frontends/lean/begin_end_annotation.cpp
+++ /dev/null
@@ -1,30 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "library/annotation.h"
-
-namespace lean {
-static name * g_begin_end = nullptr;
-static name * g_begin_end_element = nullptr;
-
-expr mk_begin_end_annotation(expr const & e) { return mk_annotation(*g_begin_end, e, nulltag); }
-expr mk_begin_end_element_annotation(expr const & e) { return mk_annotation(*g_begin_end_element, e, nulltag); }
-bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_end); }
-bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
-
-void initialize_begin_end_annotation() {
-    g_begin_end  = new name("begin_end");
-    g_begin_end_element = new name("begin_end_element");
-    register_annotation(*g_begin_end);
-    register_annotation(*g_begin_end_element);
-}
-
-void finalize_begin_end_annotation() {
-    delete g_begin_end;
-    delete g_begin_end_element;
-}
-}
diff --git a/src/frontends/lean/begin_end_annotation.h b/src/frontends/lean/begin_end_annotation.h
deleted file mode 100644
index 2d95e91933..0000000000
--- a/src/frontends/lean/begin_end_annotation.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-#include "frontends/lean/cmd_table.h"
-
-namespace lean {
-expr mk_begin_end_annotation(expr const & e);
-expr mk_begin_end_element_annotation(expr const & e);
-bool is_begin_end_annotation(expr const & e);
-bool is_begin_end_element_annotation(expr const & e);
-
-void initialize_begin_end_annotation();
-void finalize_begin_end_annotation();
-}
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 23c4e51335..1c4d2e7978 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -42,9 +42,9 @@ Author: Leonardo de Moura
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/print_cmd.h"
 #include "frontends/lean/find_cmd.h"
-#include "frontends/lean/begin_end_annotation.h"
+// #include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/decl_cmds.h"
-#include "frontends/lean/tactic_hint.h"
+// #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parse_table.h"
 
@@ -695,7 +695,7 @@ void init_cmd_table(cmd_table & r) {
     register_inductive_cmd(r);
     register_structure_cmd(r);
     register_notation_cmds(r);
-    register_tactic_hint_cmd(r);
+    // register_tactic_hint_cmd(r);
 }
 
 static cmd_table * g_cmds = nullptr;
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index a752c43bdf..e639132b63 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -27,11 +27,11 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
-#include "frontends/lean/begin_end_annotation.h"
+// #include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/info_tactic.h"
+// #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/info_annotation.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/obtain_expr.h"
diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp
deleted file mode 100644
index 34f76e2184..0000000000
--- a/src/frontends/lean/builtin_tactics.cpp
+++ /dev/null
@@ -1,139 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <library/let.h>
-#include <library/constants.h>
-#include "library/tactic/note_tactic.h"
-#include "library/tactic/generalize_tactic.h"
-#include "frontends/lean/tokens.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/parse_rewrite_tactic.h"
-#include "frontends/lean/parse_with_options_tactic.h"
-#include "frontends/lean/parse_with_attributes_tactic.h"
-
-namespace lean {
-namespace notation {
-static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_rewrite_tactic(p), pos);
-}
-
-static expr parse_xrewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_xrewrite_tactic(p), pos);
-}
-
-static expr parse_krewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_krewrite_tactic(p), pos);
-}
-
-static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_esimp_tactic(p), pos);
-}
-
-static expr parse_unfold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_unfold_tactic(p), pos);
-}
-
-static expr parse_fold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_fold_tactic(p), pos);
-}
-
-static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const &) {
-    return args[0];
-}
-
-static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
-    auto id_pos     = p.pos();
-    name id    = p.check_atomic_id_next("invalid 'let' tactic, identifier expected");
-    p.check_token_next(get_assign_tk(), "invalid 'let' tactic, ':=' expected");
-    expr value = p.parse_tactic_expr_arg();
-    // Register value as expandable local expr. Identical to let term parsing, but without surrounding mk_let.
-    value = p.save_pos(mk_let_value(value), id_pos);
-    p.add_local_expr(id, value);
-    // nothing to do, so return the id tactic
-    return p.save_pos(mk_constant(get_tactic_id_name()), pos);
-}
-
-static expr parse_note_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
-    name id    = p.check_atomic_id_next("invalid 'note' tactic, identifier expected");
-    p.check_token_next(get_assign_tk(), "invalid 'note' tactic, ':=' expected");
-    expr value = p.parse_tactic_expr_arg();
-    return p.save_pos(mk_note_tactic_expr(id, value), pos);
-}
-
-static expr parse_with_options_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_with_options_tactic(p), pos);
-}
-
-static expr parse_with_attributes_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_with_attributes_tactic(p), pos);
-}
-
-static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
-    expr e = p.parse_tactic_expr_arg();
-    name id;
-    if (p.curr_is_token(get_as_tk())) {
-        p.next();
-        id = p.check_atomic_id_next("invalid 'generalize' tactic, identifier expected");
-    } else {
-        if (is_constant(e))
-            id = const_name(e);
-        else if (is_local(e))
-            id = local_pp_name(e);
-        else
-            id = name("x");
-    }
-    return p.save_pos(mk_generalize_tactic_expr(e, id), pos);
-}
-
-parse_table init_tactic_nud_table() {
-    action Expr(mk_expr_action());
-    expr x0 = mk_var(0);
-    parse_table r;
-    r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
-    r = r.add({transition("rewrite",         mk_ext_action(parse_rewrite_tactic_expr))}, x0);
-    r = r.add({transition("krewrite",        mk_ext_action(parse_krewrite_tactic_expr))}, x0);
-    r = r.add({transition("xrewrite",        mk_ext_action(parse_xrewrite_tactic_expr))}, x0);
-    r = r.add({transition("esimp",           mk_ext_action(parse_esimp_tactic_expr))}, x0);
-    r = r.add({transition("generalize",      mk_ext_action(parse_generalize_tactic))}, x0);
-    r = r.add({transition("unfold",          mk_ext_action(parse_unfold_tactic_expr))}, x0);
-    r = r.add({transition("fold",            mk_ext_action(parse_fold_tactic_expr))}, x0);
-    r = r.add({transition("let",             mk_ext_action(parse_let_tactic))}, x0);
-    r = r.add({transition("note",            mk_ext_action(parse_note_tactic))}, x0);
-    r = r.add({transition("with_options",    mk_ext_action(parse_with_options_tactic_expr))}, x0);
-    r = r.add({transition("with_attributes", mk_ext_action(parse_with_attributes_tactic_expr))}, x0);
-    r = r.add({transition("with_attrs",      mk_ext_action(parse_with_attributes_tactic_expr))}, x0);
-    return r;
-}
-
-parse_table init_tactic_led_table() {
-    parse_table r(false);
-    return r;
-}
-}
-
-static parse_table * g_nud_table = nullptr;
-static parse_table * g_led_table = nullptr;
-
-parse_table get_builtin_tactic_nud_table() {
-    return *g_nud_table;
-}
-
-parse_table get_builtin_tactic_led_table() {
-    return *g_led_table;
-}
-
-void initialize_builtin_tactics() {
-    g_nud_table             = new parse_table();
-    *g_nud_table            = notation::init_tactic_nud_table();
-    g_led_table             = new parse_table();
-    *g_led_table            = notation::init_tactic_led_table();
-}
-
-void finalize_builtin_tactics() {
-    delete g_led_table;
-    delete g_nud_table;
-}
-}
diff --git a/src/frontends/lean/builtin_tactics.h b/src/frontends/lean/builtin_tactics.h
deleted file mode 100644
index ba788123cd..0000000000
--- a/src/frontends/lean/builtin_tactics.h
+++ /dev/null
@@ -1,14 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "frontends/lean/parse_table.h"
-namespace lean {
-parse_table get_builtin_tactic_nud_table();
-parse_table get_builtin_tactic_led_table();
-void initialize_builtin_tactics();
-void finalize_builtin_tactics();
-}
diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index 8ad3e595b5..ee461fc3d1 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -28,14 +28,13 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/begin_end_annotation.h"
 
 namespace lean {
 static name * g_calc_name  = nullptr;
 
 static expr mk_calc_annotation_core(expr const & e) { return mk_annotation(*g_calc_name, e); }
 static expr mk_calc_annotation(expr const & pr) {
-    if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) {
+    if (is_by(pr) || /* is_begin_end_annotation(pr) || */ is_sorry(pr)) {
         return pr;
     } else {
         return mk_calc_annotation_core(pr);
diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp
deleted file mode 100644
index d9b294bd9c..0000000000
--- a/src/frontends/lean/info_tactic.cpp
+++ /dev/null
@@ -1,58 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/tactic/elaborate.h"
-#include "library/tactic/expr_to_tactic.h"
-
-namespace lean {
-LEAN_THREAD_PTR(proof_state const, g_info_proof_state);
-
-optional<proof_state> get_info_tactic_proof_state() {
-    if (g_info_proof_state) {
-        return some_proof_state(*g_info_proof_state);
-    } else {
-        return none_proof_state();
-    }
-}
-
-void set_info_tactic_proof_state(proof_state const * ps) {
-    g_info_proof_state = ps;
-}
-
-struct scoped_info_tactic_proof_state {
-    scoped_info_tactic_proof_state(proof_state const & s) {
-        set_info_tactic_proof_state(&s);
-    }
-    ~scoped_info_tactic_proof_state() {
-        set_info_tactic_proof_state(nullptr);
-    }
-};
-
-tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) {
-    return tactic1([=](environment const &, io_state const & ios, proof_state const & ps) -> proof_state {
-            // create dummy variable just to communicate position to the elaborator
-            expr dummy = mk_sort(mk_level_zero(), e.get_tag());
-            scoped_info_tactic_proof_state scope(ps);
-            fn(goal(), ios.get_options(), dummy, none_expr(), substitution(), false);
-            return ps;
-        });
-}
-
-#define INFO_TAC_NAME name({"tactic", "info"})
-
-expr mk_info_tactic_expr() {
-    return mk_constant(INFO_TAC_NAME);
-}
-
-void initialize_info_tactic() {
-    register_tac(INFO_TAC_NAME,
-                 [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
-                     return mk_info_tactic(fn, e);
-                 });
-}
-void finalize_info_tactic() {
-}
-}
diff --git a/src/frontends/lean/info_tactic.h b/src/frontends/lean/info_tactic.h
deleted file mode 100644
index 2e73743e00..0000000000
--- a/src/frontends/lean/info_tactic.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/tactic/proof_state.h"
-
-namespace lean {
-expr mk_info_tactic_expr();
-/** \brief The tactic framework does not have access to the info manager.
-    Thus, it cannot store the proof_state there. The info tactic accomplishes
-    that by (temporarily) saving the proof state in a thread-local storage
-    that is accessed by the elaborator using this function. */
-optional<proof_state> get_info_tactic_proof_state();
-void initialize_info_tactic();
-void finalize_info_tactic();
-}
diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp
index f58539b5a3..821c056b43 100644
--- a/src/frontends/lean/init_module.cpp
+++ b/src/frontends/lean/init_module.cpp
@@ -9,19 +9,19 @@ Author: Leonardo de Moura
 #include "frontends/lean/old_elaborator.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/info_annotation.h"
-#include "frontends/lean/tactic_hint.h"
+// #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/calc.h"
-#include "frontends/lean/begin_end_annotation.h"
+// #include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/builtin_cmds.h"
 #include "frontends/lean/builtin_exprs.h"
-#include "frontends/lean/builtin_tactics.h"
+// #include "frontends/lean/builtin_tactics.h"
 #include "frontends/lean/inductive_cmd.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/token_table.h"
-#include "frontends/lean/info_tactic.h"
+// #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/find_cmd.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/pp.h"
@@ -31,7 +31,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/prenum.h"
-#include "frontends/lean/parse_with_attributes_tactic.h"
+// #include "frontends/lean/parse_with_attributes_tactic.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -42,19 +42,19 @@ void initialize_frontend_lean_module() {
     initialize_parse_table();
     initialize_builtin_cmds();
     initialize_builtin_exprs();
-    initialize_builtin_tactics();
+    // initialize_builtin_tactics();
     initialize_elaborator_context();
     initialize_old_elaborator();
     initialize_scanner();
     initialize_parser();
-    initialize_tactic_hint();
+    // initialize_tactic_hint();
     initialize_parser_config();
     initialize_calc();
-    initialize_begin_end_annotation();
+    // initialize_begin_end_annotation();
     initialize_inductive_cmd();
     initialize_structure_cmd();
     initialize_info_manager();
-    initialize_info_tactic();
+    // initialize_info_tactic();
     initialize_pp();
     initialize_server();
     initialize_find_cmd();
@@ -62,10 +62,10 @@ void initialize_frontend_lean_module() {
     initialize_obtain_expr();
     initialize_decl_cmds();
     initialize_nested_declaration();
-    initialize_with_attributes_tactic();
+    // initialize_with_attributes_tactic();
 }
 void finalize_frontend_lean_module() {
-    finalize_with_attributes_tactic();
+    // finalize_with_attributes_tactic();
     finalize_nested_declaration();
     finalize_decl_cmds();
     finalize_obtain_expr();
@@ -73,19 +73,19 @@ void finalize_frontend_lean_module() {
     finalize_find_cmd();
     finalize_server();
     finalize_pp();
-    finalize_info_tactic();
+    // finalize_info_tactic();
     finalize_info_manager();
     finalize_structure_cmd();
     finalize_inductive_cmd();
-    finalize_begin_end_annotation();
+    // finalize_begin_end_annotation();
     finalize_calc();
     finalize_parser_config();
-    finalize_tactic_hint();
+    // finalize_tactic_hint();
     finalize_parser();
     finalize_scanner();
     finalize_old_elaborator();
     finalize_elaborator_context();
-    finalize_builtin_tactics();
+    // finalize_builtin_tactics();
     finalize_builtin_exprs();
     finalize_builtin_cmds();
     finalize_parse_table();
diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp
index 5855546eda..e6ad673539 100644
--- a/src/frontends/lean/old_elaborator.cpp
+++ b/src/frontends/lean/old_elaborator.cpp
@@ -48,12 +48,11 @@ Author: Leonardo de Moura
 #include "library/definitional/equations.h"
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/structure_cmd.h"
-#include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/info_annotation.h"
 #include "frontends/lean/old_elaborator.h"
-#include "frontends/lean/info_tactic.h"
-#include "frontends/lean/begin_end_annotation.h"
+// #include "frontends/lean/info_tactic.h"
+// #include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/calc.h"
@@ -740,7 +739,9 @@ expr old_elaborator::visit_app(expr const & e, constraint_seq & cs) {
     }
     constraint_seq a_cs;
     expr d_type = binding_domain(f_type);
-    if (d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type() ||
+    if (false) {
+        /*
+        d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type() ||
         d_type == get_tactic_using_expr_type() || d_type == get_tactic_location_type() ||
         d_type == get_tactic_with_expr_type()) {
         expr const & a = app_arg(e);
@@ -755,6 +756,8 @@ expr old_elaborator::visit_app(expr const & e, constraint_seq & cs) {
         }
         cs += f_cs + a_cs;
         return r;
+        */
+        lean_unreachable();
     } else {
         expr a          = visit_expecting_type_of(app_arg(e), d_type, a_cs);
         expr a_type     = infer_type(a, a_cs);
@@ -1976,24 +1979,6 @@ bool old_elaborator::try_using(substitution & subst, expr const & mvar, proof_st
     }
 }
 
-static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq) {
-    if (is_begin_end_element_annotation(pre_tac)) {
-        pre_tac_seq.push_back(get_annotation_arg(pre_tac));
-    } else if (is_begin_end_annotation(pre_tac)) {
-        // nested begin-end block
-        pre_tac_seq.push_back(pre_tac);
-    } else {
-        buffer<expr> args;
-        if (get_app_args(pre_tac, args) == get_and_then_tac_fn()) {
-            for (expr const & arg : args) {
-                extract_begin_end_tactics(arg, pre_tac_seq);
-            }
-        } else {
-            throw exception("internal error, invalid begin-end tactic");
-        }
-    }
-}
-
 void old_elaborator::show_goal(proof_state const & ps, expr const & start, expr const & end, expr const & curr) {
     unsigned line, col;
     if (!m_ctx.has_show_goal_at(line, col))
@@ -2017,81 +2002,6 @@ void old_elaborator::show_goal(proof_state const & ps, expr const & start, expr
     print_lean_info_footer(out.get_stream());
 }
 
-bool old_elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
-    lean_assert(is_begin_end_annotation(pre_tac));
-    expr end_expr   = pre_tac;
-    expr start_expr = get_annotation_arg(pre_tac);
-    buffer<expr> pre_tac_seq;
-    extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq);
-    for (expr ptac : pre_tac_seq) {
-        if (is_begin_end_annotation(ptac)) {
-            goals gs = ps.get_goals();
-            if (!gs)
-                throw_elaborator_exception("invalid nested begin-end block, there are no goals to be solved", ptac);
-            goal  g             = head(gs);
-            expr mvar           = g.get_mvar();
-            proof_state focus_ps(ps, goals(g));
-            if (!try_using_begin_end(subst, mvar, focus_ps, ptac))
-                return false;
-            ps = proof_state(ps, tail(gs), subst);
-        } else {
-            show_goal(ps, start_expr, end_expr, ptac);
-            expr new_ptac = subst.instantiate_all(ptac);
-            if (auto tac = pre_tactic_to_tactic(new_ptac)) {
-                try {
-                    ps = ps.update_report_failure(true);
-                    proof_state_seq seq = (*tac)(env(), ios(), ps);
-                    auto r = seq.pull();
-                    if (!r) {
-                        // tactic failed to produce any result
-                        display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
-                        return false;
-                    }
-                    if (m_ctx.m_flycheck_goals) {
-                        if (auto p = pip()->get_pos_info(ptac)) {
-                            auto out = regular(env(), ios(), m_tc->get_type_context());
-                            flycheck_information info(ios());
-                            if (info.enabled()) {
-                                display_information_pos(out, pip()->get_file_name(), p->first, p->second);
-                                out << " proof state:\n" << ps.pp(out.get_formatter()) << "\n";
-                            }
-                        }
-                    }
-                    ps = r->first;
-                } catch (tactic_exception & ex) {
-                    display_tactic_exception(ex, ps, ptac);
-                    return false;
-                } catch (exception &) {
-                    throw;
-                } catch (throwable & ex) {
-                    auto out = regular(env(), ios(), m_tc->get_type_context());
-                    flycheck_error err(ios());
-                    if (!err.enabled() || save_error(pip(), ptac)) {
-                        display_error_pos(out, pip(), ptac);
-                        out << ex.what() << "\nproof state:\n";
-                        out << ps.pp(out.get_formatter()) << "\n";
-                    }
-                    return false;
-                }
-            } else {
-                return false;
-            }
-        }
-    }
-    show_goal(ps, start_expr, end_expr, end_expr);
-
-    if (!empty(ps.get_goals())) {
-        display_unsolved_subgoals(mvar, ps, pre_tac);
-        return false;
-    } else {
-        subst = ps.get_subst();
-        lean_assert(subst.is_assigned(mvar));
-        expr v = subst.instantiate(mvar);
-        subst.assign(mlocal_name(mvar), v);
-        return true;
-    }
-}
-
 // The parameters univs_fixed is true if the elaborator has instantiated the universe metavariables with universe parameters.
 // See issue #771
 void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited, bool reject_type_is_meta) {
@@ -2110,6 +2020,7 @@ void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name
         throw_elaborator_exception("failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) "
                                    "(solution: provide type explicitly)", mvar);
     }
+    /*
     proof_state ps = to_proof_state(*meta, type, subst);
     if (auto pre_tac = get_pre_tactic_for(mvar)) {
         if (is_begin_end_annotation(*pre_tac)) {
@@ -2134,6 +2045,8 @@ void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name
             }
         }
     }
+    */
+    return;
 }
 
 /** \brief Execute \c fn on every metavariable occurring in \c e.
@@ -2408,9 +2321,11 @@ elaborate_result old_elaborator::elaborate_nested(list<expr> const & ctx, option
                                               expr const & n, bool use_tactic_hints,
                                               substitution const & subst, bool report_unassigned) {
     if (infom()) {
+        /*
         if (auto ps = get_info_tactic_proof_state()) {
             save_proof_state_info(*ps, n);
         }
+        */
     }
     expr e = translate(env(), ctx, n);
     metavar_closure cls;
diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp
deleted file mode 100644
index 144eef8b23..0000000000
--- a/src/frontends/lean/parse_rewrite_tactic.cpp
+++ /dev/null
@@ -1,226 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/tactic/rewrite_tactic.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/tokens.h"
-#include "frontends/lean/parse_tactic_location.h"
-
-namespace lean {
-static optional<expr> parse_pattern(parser & p) {
-    if (p.curr_is_token(get_lcurly_tk())) {
-        p.next();
-        expr r = p.parse_tactic_expr_arg();
-        p.check_token_next(get_rcurly_tk(), "invalid rewrite pattern, '}' expected");
-        return some_expr(r);
-    } else {
-        return none_expr();
-    }
-}
-
-static expr parse_rule(parser & p, bool use_paren) {
-    if (use_paren) {
-        if (p.curr_is_token(get_lparen_tk())) {
-            p.next();
-            expr r = p.parse_tactic_expr_arg();
-            p.check_token_next(get_rparen_tk(), "invalid rewrite pattern, ')' expected");
-            return r;
-        } else {
-            return p.parse_tactic_id_arg();
-        }
-    } else {
-        return p.parse_tactic_expr_arg();
-    }
-}
-
-static void check_not_in_theorem_queue(parser & p, name const & n, pos_info const & pos) {
-    if (p.in_theorem_queue(n)) {
-        throw parser_error(sstream() << "invalid 'rewrite' tactic, cannot unfold '" << n << "' "
-                           << "which is still in the theorem queue. Use command 'reveal " << n << "' "
-                           << "to access its definition.", pos);
-    }
-}
-
-static expr parse_rewrite_unfold_core(parser & p, bool force_unfold) {
-    buffer<name> to_unfold;
-    if (p.curr_is_token(get_lbracket_tk())) {
-        p.next();
-        while (true) {
-            auto pos = p.pos();
-            to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier expected"));
-            check_not_in_theorem_queue(p, to_unfold.back(), pos);
-            if (!p.curr_is_token(get_comma_tk()))
-                break;
-            p.next();
-        }
-        p.check_token_next(get_rbracket_tk(), "invalid unfold rewrite step, ',' or ']' expected");
-    } else {
-        auto pos = p.pos();
-        to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier or '[' expected"));
-        check_not_in_theorem_queue(p, to_unfold.back(), pos);
-    }
-    location loc = parse_tactic_location(p);
-    return mk_rewrite_unfold(to_list(to_unfold), force_unfold, loc);
-}
-
-static expr parse_rewrite_unfold(parser & p, bool force_unfold) {
-    lean_assert(p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk()));
-    p.next();
-    return parse_rewrite_unfold_core(p, force_unfold);
-}
-
-// If use_paren is true, then lemmas must be identifiers or be wrapped with parenthesis
-static expr parse_rewrite_element(parser & p, bool use_paren) {
-    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
-        bool force_unfold = true;
-        return parse_rewrite_unfold(p, force_unfold);
-    }
-    if (p.curr_is_token(get_down_tk())) {
-        p.next();
-        expr e = p.parse_tactic_expr_arg();
-        location loc = parse_tactic_location(p);
-        return mk_rewrite_fold(e, loc);
-    }
-    bool symm = false;
-    if (p.curr_is_token(get_sub_tk())) {
-        p.next();
-        symm = true;
-    }
-    if (p.curr_is_numeral()) {
-        unsigned n = p.parse_small_nat();
-        if (p.curr_is_token(get_greater_tk())) {
-            p.next();
-            optional<expr> pat = parse_pattern(p);
-            expr H = parse_rule(p, use_paren);
-            location loc = parse_tactic_location(p);
-            return mk_rewrite_at_most_n(pat, H, symm, n, loc);
-        } else {
-            optional<expr> pat = parse_pattern(p);
-            expr H = parse_rule(p, use_paren);
-            location loc = parse_tactic_location(p);
-            return mk_rewrite_exactly_n(pat, H, symm, n, loc);
-        }
-    } else if (p.curr_is_token(get_star_tk())) {
-        p.next();
-        optional<expr> pat = parse_pattern(p);
-        expr H = parse_rule(p, use_paren);
-        location loc = parse_tactic_location(p);
-        return mk_rewrite_zero_or_more(pat, H, symm, loc);
-    } else if (p.curr_is_token(get_plus_tk())) {
-        p.next();
-        optional<expr> pat = parse_pattern(p);
-        expr H = parse_rule(p, use_paren);
-        location loc = parse_tactic_location(p);
-        return mk_rewrite_one_or_more(pat, H, symm, loc);
-    } else if (p.curr_is_token(get_triangle_tk()) || p.curr_is_token(get_greater_tk())) {
-        p.next();
-        if (p.curr_is_token(get_star_tk())) {
-            p.next();
-            location loc = parse_tactic_location(p);
-            return mk_rewrite_reduce(loc);
-        } else {
-            expr e = p.parse_tactic_expr_arg();
-            location loc = parse_tactic_location(p);
-            return mk_rewrite_reduce_to(e, loc);
-        }
-    } else {
-        optional<expr> pat = parse_pattern(p);
-        expr H = parse_rule(p, use_paren);
-        location loc = parse_tactic_location(p);
-        return mk_rewrite_once(pat, H, symm, loc);
-    }
-}
-
-void parse_rewrite_tactic_elems(parser & p, buffer<expr> & elems) {
-    if (p.curr_is_token(get_lbracket_tk())) {
-        p.next();
-        while (!p.curr_is_token(get_rbracket_tk())) {
-            auto pos = p.pos();
-            elems.push_back(p.save_pos(parse_rewrite_element(p, false), pos));
-            if (!p.curr_is_token(get_comma_tk()))
-                break;
-            p.next();
-        }
-        p.next();
-    } else {
-        auto pos = p.pos();
-        elems.push_back(p.save_pos(parse_rewrite_element(p, true), pos));
-    }
-}
-
-expr parse_rewrite_tactic(parser & p) {
-    buffer<expr> elems;
-    parse_rewrite_tactic_elems(p, elems);
-    return mk_rewrite_tactic_expr(elems);
-}
-
-expr parse_xrewrite_tactic(parser & p) {
-    buffer<expr> elems;
-    parse_rewrite_tactic_elems(p, elems);
-    return mk_xrewrite_tactic_expr(elems);
-}
-
-expr parse_krewrite_tactic(parser & p) {
-    buffer<expr> elems;
-    parse_rewrite_tactic_elems(p, elems);
-    return mk_krewrite_tactic_expr(elems);
-}
-
-expr parse_esimp_tactic(parser & p) {
-    buffer<expr> elems;
-    auto pos = p.pos();
-    bool force_unfold = false;
-    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
-        elems.push_back(p.save_pos(parse_rewrite_unfold(p, force_unfold), pos));
-    } else if (p.curr_is_token(get_lbracket_tk())) {
-        elems.push_back(p.save_pos(parse_rewrite_unfold_core(p, force_unfold), pos));
-    } else {
-        location loc = parse_tactic_location(p);
-        elems.push_back(p.save_pos(mk_rewrite_reduce(loc), pos));
-    }
-    return mk_rewrite_tactic_expr(elems);
-}
-
-expr parse_unfold_tactic(parser & p) {
-    buffer<expr> elems;
-    auto pos = p.pos();
-    bool force_unfold = true;
-    if (p.curr_is_identifier()) {
-        name c       = p.check_constant_next("invalid unfold tactic, identifier expected");
-        check_not_in_theorem_queue(p, c, pos);
-        location loc = parse_tactic_location(p);
-        elems.push_back(p.save_pos(mk_rewrite_unfold(to_list(c), force_unfold, loc), pos));
-    } else if (p.curr_is_token(get_lbracket_tk())) {
-        elems.push_back(p.save_pos(parse_rewrite_unfold_core(p, force_unfold), pos));
-    } else {
-        throw parser_error("invalid unfold tactic, identifier or `[` expected", pos);
-    }
-    return mk_rewrite_tactic_expr(elems);
-}
-
-expr parse_fold_tactic(parser & p) {
-    buffer<expr> elems;
-    auto pos = p.pos();
-    if (p.curr_is_token(get_lbracket_tk())) {
-        p.next();
-        while (true) {
-            auto pos = p.pos();
-            expr e = p.parse_tactic_expr_arg();
-            location loc = parse_tactic_location(p);
-            elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos));
-            if (!p.curr_is_token(get_comma_tk()))
-                break;
-            p.next();
-        }
-        p.check_token_next(get_rbracket_tk(), "invalid 'fold' tactic, ',' or ']' expected");
-    } else {
-        expr e = p.parse_tactic_expr_arg();
-        location loc = parse_tactic_location(p);
-        elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos));;
-    }
-    return mk_rewrite_tactic_expr(elems);
-}
-}
diff --git a/src/frontends/lean/parse_rewrite_tactic.h b/src/frontends/lean/parse_rewrite_tactic.h
deleted file mode 100644
index 367cb73180..0000000000
--- a/src/frontends/lean/parse_rewrite_tactic.h
+++ /dev/null
@@ -1,18 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-class parser;
-expr parse_rewrite_tactic(parser & p);
-expr parse_krewrite_tactic(parser & p);
-expr parse_xrewrite_tactic(parser & p);
-expr parse_esimp_tactic(parser & p);
-expr parse_unfold_tactic(parser & p);
-expr parse_fold_tactic(parser & p);
-}
diff --git a/src/frontends/lean/parse_tactic_location.cpp b/src/frontends/lean/parse_tactic_location.cpp
deleted file mode 100644
index b36880c073..0000000000
--- a/src/frontends/lean/parse_tactic_location.cpp
+++ /dev/null
@@ -1,96 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/tactic/location.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/tokens.h"
-#include "frontends/lean/parse_tactic_location.h"
-
-namespace lean {
-static occurrence parse_occurrence(parser & p) {
-    bool is_pos = true;
-    if (p.curr_is_token(get_sub_tk())) {
-        p.next();
-        is_pos = false;
-        if (!p.curr_is_token(get_lcurly_tk()))
-            throw parser_error("invalid tactic location, '{' expected", p.pos());
-    }
-    if (p.curr_is_token(get_lcurly_tk())) {
-        p.next();
-        buffer<unsigned> occs;
-        while (true) {
-            auto pos   = p.pos();
-            unsigned i = p.parse_small_nat();
-            if (i == 0)
-                throw parser_error("invalid tactic location, first occurrence is 1", pos);
-            occs.push_back(i);
-            if (!p.curr_is_token(get_comma_tk()))
-                break;
-            p.next();
-        }
-        p.check_token_next(get_rcurly_tk(), "invalid tactic location, '}' or ',' expected");
-        if (is_pos)
-            return occurrence::mk_occurrences(occs);
-        else
-            return occurrence::mk_except_occurrences(occs);
-    } else {
-        return occurrence();
-    }
-}
-
-location parse_tactic_location(parser & p) {
-    if (p.curr_is_token(get_at_tk())) {
-        p.next();
-        if (p.curr_is_token(get_star_tk())) {
-            p.next();
-            if (p.curr_is_token(get_turnstile_tk())) {
-                p.next();
-                if (p.curr_is_token(get_star_tk())) {
-                    // at * |- *
-                    return location::mk_everywhere();
-                } else {
-                    // at * |-
-                    return location::mk_all_hypotheses();
-                }
-            } else {
-                // at *
-                return location::mk_everywhere();
-            }
-        } else if (p.curr_is_token(get_lparen_tk())) {
-            p.next();
-            buffer<name>       hyps;
-            buffer<occurrence> hyp_occs;
-            while (true) {
-                hyps.push_back(p.get_name_val());
-                p.next();
-                hyp_occs.push_back(parse_occurrence(p));
-                if (!p.curr_is_token(get_comma_tk()))
-                    break;
-                p.next();
-            }
-            p.check_token_next(get_rparen_tk(), "invalid tactic location, ')' expected");
-            if (p.curr_is_token(get_turnstile_tk())) {
-                p.next();
-                occurrence goal_occ = parse_occurrence(p);
-                return location::mk_at(goal_occ, hyps, hyp_occs);
-            } else {
-                return location::mk_hypotheses_at(hyps, hyp_occs);
-            }
-        } else if (p.curr_is_token(get_lcurly_tk()) || p.curr_is_token(get_sub_tk())) {
-            occurrence o = parse_occurrence(p);
-            return location::mk_goal_at(o);
-        } else {
-            buffer<name>       hyps;
-            buffer<occurrence> hyp_occs;
-            hyps.push_back(p.check_id_next("invalid tactic location, identifier expected"));
-            hyp_occs.push_back(parse_occurrence(p));
-            return location::mk_hypotheses_at(hyps, hyp_occs);
-        }
-    } else {
-        return location::mk_goal_only();
-    }
-}
-}
diff --git a/src/frontends/lean/parse_tactic_location.h b/src/frontends/lean/parse_tactic_location.h
deleted file mode 100644
index 8a28851af2..0000000000
--- a/src/frontends/lean/parse_tactic_location.h
+++ /dev/null
@@ -1,13 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/tactic/location.h"
-
-namespace lean {
-class parser;
-location parse_tactic_location(parser & p);
-}
diff --git a/src/frontends/lean/parse_with_attributes_tactic.cpp b/src/frontends/lean/parse_with_attributes_tactic.cpp
deleted file mode 100644
index d5cf7522e3..0000000000
--- a/src/frontends/lean/parse_with_attributes_tactic.cpp
+++ /dev/null
@@ -1,120 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "library/constants.h"
-#include "library/scoped_ext.h"
-#include "library/kernel_serializer.h"
-#include "library/tactic/expr_to_tactic.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/decl_attributes.h"
-
-namespace lean {
-static name * g_name             = nullptr;
-static std::string * g_opcode    = nullptr;
-
-// Auxiliary macro for wrapping decl_attributes object as an expression
-class attributes_macro_cell : public macro_definition_cell {
-    decl_attributes m_decl;
-public:
-    attributes_macro_cell(decl_attributes const & decl):m_decl(decl) {}
-    virtual name get_name() const { return *g_name; }
-    virtual void write(serializer & s) const { s << *g_opcode; m_decl.write(s); }
-    virtual expr check_type(expr const &, abstract_type_context &, bool) const {
-        return mk_constant(get_tactic_expr_name());
-    }
-    virtual optional<expr> expand(expr const &, abstract_type_context &) const {
-        return some_expr(mk_constant(get_tactic_expr_builtin_name()));
-    }
-    virtual bool operator==(macro_definition_cell const & other) const {
-        if (auto o = dynamic_cast<attributes_macro_cell const *>(&other))
-            return m_decl == o->m_decl;
-        return false;
-    }
-    decl_attributes const & get_attrs() const { return m_decl; }
-};
-
-expr mk_attributes_expr(decl_attributes const & d) {
-    macro_definition def(new attributes_macro_cell(d));
-    return mk_macro(def);
-}
-
-bool is_attributes_expr(expr const & e) {
-    return is_macro(e) && macro_def(e).get_name() == *g_name;
-}
-
-decl_attributes const & get_attributes_expr_attributes(expr const & e) {
-    lean_assert(is_attributes_expr(e));
-    return static_cast<attributes_macro_cell const*>(macro_def(e).raw())->get_attrs();
-}
-
-static expr * g_with_attributes_tac = nullptr;
-
-expr mk_with_attributes_tactic_expr(decl_attributes const & a, buffer<name> const & cs, expr const & t) {
-    return mk_app(*g_with_attributes_tac, mk_attributes_expr(a), ids_to_tactic_expr(cs), t);
-}
-
-tactic with_attributes(decl_attributes const & d, list<name> const & cs, tactic const & t) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
-            environment new_env = env;
-            for (name const & c : cs)
-                new_env = d.apply(new_env, ios, c, get_namespace(new_env));
-            return t(new_env, ios, s);
-        });
-}
-
-expr parse_with_attributes_tactic(parser & p) {
-    buffer<name> cs;
-    bool persistent   = false;
-    bool abbrev       = false;
-    decl_attributes attributes(abbrev, persistent);
-    name c            = p.check_constant_next("invalid 'with_attributes' tactical, constant expected");
-    cs.push_back(c);
-    while (p.curr_is_identifier()) {
-        cs.push_back(p.check_constant_next("invalid 'with_attributes' tactical, constant expected"));
-    }
-    attributes.parse(p);
-    expr t = p.parse_tactic(get_max_prec());
-    return mk_with_attributes_tactic_expr(attributes, cs, t);
-}
-
-void initialize_with_attributes_tactic() {
-    g_name     = new name("attributes");
-    g_opcode   = new std::string("ATTRS");
-    register_macro_deserializer(*g_opcode,
-                                [](deserializer & d, unsigned num, expr const *) {
-                                    if (num > 0)
-                                        throw corrupted_stream_exception();
-                                    decl_attributes attrs;
-                                    attrs.read(d);
-                                    return mk_attributes_expr(attrs);
-                                });
-
-    name with_attributes_tac_name{"tactic", "with_attributes_tac"};
-    g_with_attributes_tac = new expr(Const(with_attributes_tac_name));
-    register_tac(with_attributes_tac_name,
-                 [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
-                     buffer<expr> args;
-                     get_app_args(e, args);
-                     if (args.size() != 3)
-                         throw expr_to_tactic_exception(e, "invalid 'with_attributes' tactical, it must have two arguments");
-                     check_tactic_expr(args[0], "invalid 'with_attributes' tactical, invalid argument");
-                     expr attrs = get_tactic_expr_expr(args[0]);
-                     if (!is_attributes_expr(attrs))
-                         throw expr_to_tactic_exception(args[0], "invalid 'with_attributes' tactical, invalid argument");
-                     buffer<name> cs;
-                     get_tactic_id_list_elements(args[1], cs, "invalid 'with_attributes' tactical, invalid argument");
-                     tactic t  = expr_to_tactic(tc, fn, args[2], p);
-                     return with_attributes(get_attributes_expr_attributes(attrs), to_list(cs), t);
-                 });
-}
-
-void finalize_with_attributes_tactic() {
-    delete g_name;
-    delete g_opcode;
-    delete g_with_attributes_tac;
-}
-}
diff --git a/src/frontends/lean/parse_with_attributes_tactic.h b/src/frontends/lean/parse_with_attributes_tactic.h
deleted file mode 100644
index 8914bed3db..0000000000
--- a/src/frontends/lean/parse_with_attributes_tactic.h
+++ /dev/null
@@ -1,15 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-class parser;
-expr parse_with_attributes_tactic(parser & p);
-void initialize_with_attributes_tactic();
-void finalize_with_attributes_tactic();
-}
diff --git a/src/frontends/lean/parse_with_options_tactic.cpp b/src/frontends/lean/parse_with_options_tactic.cpp
deleted file mode 100644
index e5b0dc40d9..0000000000
--- a/src/frontends/lean/parse_with_options_tactic.cpp
+++ /dev/null
@@ -1,49 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/sexpr/option_declarations.h"
-#include "library/tactic/with_options_tactic.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/tokens.h"
-#include "frontends/lean/util.h"
-
-namespace lean {
-expr parse_with_options_tactic(parser & p) {
-    options o;
-    p.check_token_next(get_lbracket_tk(), "invalid 'with_options' tactical, '[' expected");
-    while (true) {
-        auto id_kind = parse_option_name(p, "invalid 'with_options' tactical, identifier (i.e., option name) expected");
-        name id       = id_kind.first;
-        option_kind k = id_kind.second;
-        if (k == BoolOption) {
-            if (p.curr_is_token_or_id(get_true_tk()))
-                o = o.update(id, true);
-            else if (p.curr_is_token_or_id(get_false_tk()))
-                o = o.update(id, false);
-            else
-                throw parser_error("invalid Boolean option value, 'true' or 'false' expected", p.pos());
-            p.next();
-        } else if (k == StringOption) {
-            if (!p.curr_is_string())
-                throw parser_error("invalid option value, given option is not a string", p.pos());
-            o = o.update(id, p.get_str_val());
-            p.next();
-        } else if (k == DoubleOption) {
-            o = o.update(id, p.parse_double());
-        } else if (k == UnsignedOption || k == IntOption) {
-            o = o.update(id, p.parse_small_nat());
-        } else {
-            throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", p.pos());
-        }
-        if (!p.curr_is_token(get_comma_tk()))
-            break;
-        p.next();
-    }
-    p.check_token_next(get_rbracket_tk(), "invalid 'with_options' tactical, ']' expected");
-    expr t = p.parse_tactic(get_max_prec());
-    return mk_with_options_tactic_expr(o, t);
-}
-}
diff --git a/src/frontends/lean/parse_with_options_tactic.h b/src/frontends/lean/parse_with_options_tactic.h
deleted file mode 100644
index b3b7f765a8..0000000000
--- a/src/frontends/lean/parse_with_options_tactic.h
+++ /dev/null
@@ -1,13 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-class parser;
-expr parse_with_options_tactic(parser & p);
-}
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index a9f1a9d3c0..9e2c18aba7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -49,8 +49,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/info_annotation.h"
-#include "frontends/lean/parse_rewrite_tactic.h"
-#include "frontends/lean/parse_tactic_location.h"
+// #include "frontends/lean/parse_rewrite_tactic.h"
+// #include "frontends/lean/parse_tactic_location.h"
 #include "frontends/lean/update_environment_exception.h"
 #include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/opt_cmd.h"
@@ -2004,9 +2004,11 @@ expr parser::parse_tactic_nud() {
                     check_token_next(get_with_tk(), "invalid tactic expression, 'with' expected");
                     expr e = parse_expr();
                     r = mk_app(r, e, id_pos);
+/*
                 } else if (is_tactic_location_type(d)) {
                     location l = parse_tactic_location(*this);
                     r = mk_app(r, mk_location_expr(l), id_pos);
+*/
                 } else {
                     unsigned rbp;
                     if ((arity == 1) ||
diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp
index a45a78e188..ba8077e334 100644
--- a/src/frontends/lean/parser_config.cpp
+++ b/src/frontends/lean/parser_config.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/kernel_serializer.h"
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/builtin_exprs.h"
-#include "frontends/lean/builtin_tactics.h"
 #include "frontends/lean/builtin_cmds.h"
 
 namespace lean {
@@ -227,9 +226,10 @@ struct notation_state {
         m_nud(get_builtin_nud_table()),
         m_led(get_builtin_led_table()),
         m_reserved_nud(true),
-        m_reserved_led(false),
-        m_tactic_nud(get_builtin_tactic_nud_table()),
-        m_tactic_led(get_builtin_tactic_led_table()) {
+        m_reserved_led(false)
+        {
+        // m_tactic_nud(get_builtin_tactic_nud_table()),
+        // m_tactic_led(get_builtin_tactic_led_table()) {
     }
 
     parse_table & nud(notation_entry_group g) {
diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp
deleted file mode 100644
index 2c5f5009e6..0000000000
--- a/src/frontends/lean/tactic_hint.cpp
+++ /dev/null
@@ -1,96 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "util/sstream.h"
-#include "kernel/type_checker.h"
-#include "library/scoped_ext.h"
-#include "library/constants.h"
-#include "library/kernel_serializer.h"
-#include "library/tactic/tactic.h"
-#include "frontends/lean/tactic_hint.h"
-#include "frontends/lean/cmd_table.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/tokens.h"
-
-namespace lean {
-typedef list<expr> tactic_hints;
-
-static name * g_class_name = nullptr;
-static std::string * g_key = nullptr;
-
-struct tactic_hint_config {
-    typedef tactic_hints   state;
-    typedef expr           entry;
-
-    static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
-        s = cons(e, filter(s, [&](expr const & e1) { return e1 != e; }));
-    }
-
-    static name const & get_class_name() {
-        return *g_class_name;
-    }
-
-    static std::string const & get_serialization_key() {
-        return *g_key;
-    }
-
-    static void  write_entry(serializer & s, entry const & e) {
-        s << e;
-    }
-
-    static entry read_entry(deserializer & d) {
-        entry e;
-        d >> e;
-        return e;
-    }
-
-    static optional<unsigned> get_fingerprint(entry const & e) {
-        return some(e.hash());
-    }
-};
-
-template class scoped_ext<tactic_hint_config>;
-typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
-
-void initialize_tactic_hint() {
-    g_class_name = new name("tactic");
-    g_key        = new std::string("TACHINT");
-    tactic_hint_ext::initialize();
-}
-
-void finalize_tactic_hint() {
-    tactic_hint_ext::finalize();
-    delete g_key;
-    delete g_class_name;
-}
-
-list<expr> const & get_tactic_hints(environment const & env) {
-    return tactic_hint_ext::get_state(env);
-}
-
-expr parse_tactic_name(parser & p) {
-    auto pos = p.pos();
-    name pre_tac = p.check_constant_next("invalid tactic name, constant expected");
-    auto decl    = p.env().get(pre_tac);
-    expr pre_tac_type = decl.get_type();
-    if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != get_tactic_name())
-        throw parser_error(sstream() << "invalid tactic name, '" << pre_tac << "' is not a tactic", pos);
-    buffer<level> ls;
-    for (auto const & n : decl.get_univ_params())
-        ls.push_back(mk_meta_univ(n));
-    return mk_constant(pre_tac, to_list(ls.begin(), ls.end()));
-}
-
-environment tactic_hint_cmd(parser & p) {
-    expr pre_tac = parse_tactic_name(p);
-    return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), pre_tac, get_namespace(p.env()), true);
-}
-
-void register_tactic_hint_cmd(cmd_table & r) {
-    add_cmd(r, cmd_info("tactic_hint",   "add a new tactic hint", tactic_hint_cmd));
-}
-}
diff --git a/src/frontends/lean/tactic_hint.h b/src/frontends/lean/tactic_hint.h
deleted file mode 100644
index 5809ff2a44..0000000000
--- a/src/frontends/lean/tactic_hint.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/tactic/tactic.h"
-#include "frontends/lean/cmd_table.h"
-
-namespace lean {
-list<expr> const & get_tactic_hints(environment const & env);
-class parser;
-expr parse_tactic_name(parser & p);
-void register_tactic_hint_cmd(cmd_table & r);
-
-void initialize_tactic_hint();
-void finalize_tactic_hint();
-}