diff --git a/src/Lean.lean b/src/Lean.lean
index 99af7ba85f..8ef1524375 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -24,6 +24,6 @@ import Lean.Structure
 import Lean.Delaborator
 import Lean.PrettyPrinter
 import Lean.CoreM
-
+import Lean.InternalExceptionId
 -- import only for `[init]` side-effects
 import Lean.PrettyPrinter.Meta
diff --git a/src/Lean/InternalExceptionId.lean b/src/Lean/InternalExceptionId.lean
new file mode 100644
index 0000000000..f4503fe5d6
--- /dev/null
+++ b/src/Lean/InternalExceptionId.lean
@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+namespace Lean
+
+structure InternalExceptionId :=
+(id : Nat)
+
+def mkInternalExceptionsRef : IO (IO.Ref (Array Name)) :=
+IO.mkRef #[]
+
+@[init mkInternalExceptionsRef] constant internalExceptionsRef : IO.Ref (Array Name) := arbitrary _
+
+def registerInternalExceptionId (name : Name) : IO InternalExceptionId := do
+exs ← internalExceptionsRef.get;
+when (exs.contains name) $ throw $ IO.userError ("invalid internal exception id, '" ++ toString name ++ "' has already been used");
+let nextId := exs.size;
+internalExceptionsRef.modify fun a => a.push name;
+pure { id := nextId }
+
+def InternalExceptionId.toString (id : InternalExceptionId) : IO Name :=  do
+exs ← internalExceptionsRef.get;
+pure $ exs.get! id.id
+
+end Lean