diff --git a/KLR/Trace/Builtin.lean b/KLR/Trace/Builtin.lean
index be9d9519..376d77d1 100644
--- a/KLR/Trace/Builtin.lean
+++ b/KLR/Trace/Builtin.lean
@@ -31,6 +31,7 @@ open Lean Elab Command Term Meta
 
 def nki_ : Name := .str .anonymous "nki"
 def nki_isa : Name := .str nki_ "isa"
+def nki_stdlib : Name := .str nki_ "stdlib"
 def nki_lang : Name := .str nki_ "language"
 def nki_typing : Name := .str nki_ "typing"
 
diff --git a/KLR/Trace/NKI.lean b/KLR/Trace/NKI.lean
index 94603710..4e37d921 100644
--- a/KLR/Trace/NKI.lean
+++ b/KLR/Trace/NKI.lean
@@ -38,6 +38,7 @@ def NKIEnv : List (Name × Term) :=
   [ module nki_
   , module nki_isa
   , module nki_lang
+  , module nki_stdlib  
   , module nki_typing
   , module `math
   , module `numpy
diff --git a/KLR/Trace/Term.lean b/KLR/Trace/Term.lean
index e1df1e1e..9a07dd3f 100644
--- a/KLR/Trace/Term.lean
+++ b/KLR/Trace/Term.lean
@@ -678,6 +678,5 @@ def builtinEnv : List (Name × Term) := Id.run do
       | .str `builtin.python n => [.str `builtins n, .str .anonymous n]
       | .str `builtin.isa n => [nisa n, name]
       | .str `builtin.typing n => [nt n, name]
-      | .str `builtin.lang n => [nl n, name]
       | _ => [name]
     names.map fun n => (n, fn)