diff --git a/KLR/Trace/Term.lean b/KLR/Trace/Term.lean index e1df1e1e..e6b8092f 100644 --- a/KLR/Trace/Term.lean +++ b/KLR/Trace/Term.lean @@ -676,7 +676,6 @@ def builtinEnv : List (Name × Term) := Id.run do let fn := .builtin name none let names : List Name := match name with | .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]