diff --git a/library/init/meta/converter.lean b/library/init/meta/converter.lean
index e298b46ead..220a2ad0ab 100644
--- a/library/init/meta/converter.lean
+++ b/library/init/meta/converter.lean
@@ -80,7 +80,7 @@ meta instance : alternative conv :=
   orelse  := @conv.orelse }
 
 meta def whnf_core (m : transparency) : conv unit :=
-λ r e, do n ← whnf_core m e, return ⟨(), n, none⟩
+λ r e, do n ← tactic.whnf_core m e, return ⟨(), n, none⟩
 
 meta def whnf : conv unit :=
 conv.whnf_core reducible
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 4fe02769d7..1cad526179 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -211,7 +211,7 @@ do fmt ← pp a,
    return $ _root_.trace_fmt fmt (λ u, ())
 
 meta def trace_call_stack : tactic unit :=
-take state, trace_call_stack (success () state)
+take state, _root_.trace_call_stack (success () state)
 
 meta def trace_state : tactic unit :=
 do s ← read,
diff --git a/library/tools/super/prover.lean b/library/tools/super/prover.lean
index 1042adf906..d1f2610715 100644
--- a/library/tools/super/prover.lean
+++ b/library/tools/super/prover.lean
@@ -120,6 +120,6 @@ meta def super (extra_clause_names : types.raw_ident_list)
                (extra_lemma_names : types.with_ident_list) : tactic unit := do
 with_lemmas extra_clause_names,
 extra_lemmas ← monad.for extra_lemma_names mk_const,
-super extra_lemmas
+_root_.super extra_lemmas
 
 end tactic.interactive
diff --git a/library/tools/super/prover_state.lean b/library/tools/super/prover_state.lean
index 0ecc8202c8..526e852a21 100644
--- a/library/tools/super/prover_state.lean
+++ b/library/tools/super/prover_state.lean
@@ -145,7 +145,7 @@ meta instance (α : Type) : has_coe (tactic α) (prover α) :=
 ⟨monad.monad_lift⟩
 
 meta def fail {α β : Type} [has_to_format β] (msg : β) : prover α :=
-fail msg
+tactic.fail msg
 
 meta def orelse (A : Type) (p1 p2 : prover A) : prover A :=
 take state, p1 state <|> p2 state
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 9620c189e8..f66771f3bd 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -170,7 +170,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
 }
 
 static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
-                                  bool is_example, bool is_instance) {
+                                  bool is_example, bool is_instance, bool is_meta) {
     parser::local_scope scope1(p);
     auto header_pos = p.pos();
     bool allow_default = true;
@@ -179,7 +179,19 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
     expr val;
     if (p.curr_is_token(get_assign_tk())) {
         p.next();
-        val = p.parse_expr();
+        if (is_meta) {
+            declaration_name_scope scope2("_main");
+            fn = mk_local(mlocal_name(fn), local_pp_name(fn), mlocal_type(fn), mk_rec_info(true));
+            p.add_local(fn);
+            val = p.parse_expr();
+            /* add fake equation */
+            expr eqn = mk_equation(fn, val);
+            buffer<expr> eqns;
+            eqns.push_back(eqn);
+            val = mk_equations(p, fn, scope2.get_name(), eqns, {}, header_pos);
+        } else {
+            val = p.parse_expr();
+        }
     } else if (p.curr_is_token(get_bar_tk()) || p.curr_is_token(get_period_tk())) {
         declaration_name_scope scope2("_main");
         fn = mk_local(mlocal_name(fn), local_pp_name(fn), mlocal_type(fn), mk_rec_info(true));
@@ -772,7 +784,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     bool is_rfl      = false;
     if (is_instance)
         attrs.set_attribute(p.env(), "instance");
-    std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance);
+    std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, modifiers.m_is_meta);
     p.declare_sorry_if_used();
 
     // skip elaboration of definitions during reparsing