diff --git a/library/init/default.lean b/library/init/default.lean
index ad412bd4da..df9b1fc5f9 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -13,4 +13,4 @@ import init.monad_combinators
 import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
 import init.wf init.nat_div init.meta init.instances
 import init.wf_k init.sigma_lex
-import init.simplifier
+import init.simplifier init.id_locked
diff --git a/library/init/id_locked.lean b/library/init/id_locked.lean
new file mode 100644
index 0000000000..1f93348a8d
--- /dev/null
+++ b/library/init/id_locked.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic init.meta.constructor_tactic
+open tactic
+
+/-
+  Define id_locked using meta-programming because we don't have
+  syntax for setting reducibility_hints.
+
+  See module init.meta.declaration.
+-/
+run_command do
+ l  ← return $ level.param `l,
+ Ty ← return $ expr.sort l,
+ type ← to_expr `(Π {A : %%Ty}, A → A),
+ val  ← to_expr `(λ {A : %%Ty} (a : A), a),
+ add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)
+
+lemma id_locked_eq {A : Type} (a : A) : id_locked a = a :=
+rfl