diff --git a/library/standard/logic.lean b/library/standard/logic.lean
index 9f9dfcdf7c..bc1aa98d63 100644
--- a/library/standard/logic.lean
+++ b/library/standard/logic.lean
@@ -85,8 +85,7 @@ theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀
 definition cast {A B : Type} (H : A = B) (a : A) : B
 := eq_rec a H
 
--- TODO(Leo): check why unifier needs 'help' in the following theorem
-theorem cast_refl.{l} {A : Type.{l}} (a : A) : cast (refl A) a = a
+theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a
 := refl (cast (refl A) a)
 
 definition iff (a b : Bool) := (a → b) ∧ (b → a)
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 9917660700..c1c2ba2255 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -798,8 +798,8 @@ optional<expr> inductive_normalizer_extension::operator()(expr const & e, extens
     for (unsigned i = 0; i < it2->m_num_bu; i++)
         ACebu.push_back(intro_args[it1->m_num_params + i]);
     std::reverse(ACebu.begin(), ACebu.end());
-    expr r = instantiate(it2->m_comp_rhs_body, ACebu.size(), ACebu.data());
-    r = instantiate_univ_params(r, it1->m_level_names, const_levels(elim_fn));
+    expr r = instantiate_univ_params(it2->m_comp_rhs_body, it1->m_level_names, const_levels(elim_fn));
+    r = instantiate(r, ACebu.size(), ACebu.data());
     return some_expr(r);
 }