diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean
index dad9d787b3..442a52fb37 100644
--- a/src/Lean/Meta/DiscrTreeTypes.lean
+++ b/src/Lean/Meta/DiscrTreeTypes.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -5,8 +6,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Expr
 
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 
 /- See file `DiscrTree.lean` for the actual implementation and documentation. -/
 
@@ -19,18 +19,18 @@ inductive Key
 | star  : Key
 | other : Key
 
-instance Key.inhabited : Inhabited Key := ⟨Key.star⟩
+instance : Inhabited Key := ⟨Key.star⟩
 
-def Key.hash : Key → USize
+protected def Key.hash : Key → USize
 | Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a)
 | Key.fvar n a  => mixHash 3541 $ mixHash (hash n) (hash a)
 | Key.lit v     => mixHash 1879 $ hash v
 | Key.star      => 7883
 | Key.other     => 2411
 
-instance Key.hashable : Hashable Key := ⟨Key.hash⟩
+instance : Hashable Key := ⟨Key.hash⟩
 
-def Key.beq : Key → Key → Bool
+protected def Key.beq : Key → Key → Bool
 | Key.const c₁ a₁, Key.const c₂ a₂ => c₁ == c₂ && a₁ == a₂
 | Key.fvar c₁ a₁,  Key.fvar c₂ a₂  => c₁ == c₂ && a₁ == a₂
 | Key.lit v₁,      Key.lit v₂      => v₁ == v₂
@@ -38,10 +38,10 @@ def Key.beq : Key → Key → Bool
 | Key.other,       Key.other       => true
 | _,                _              => false
 
-instance Key.hasBeq : HasBeq Key := ⟨Key.beq⟩
+instance : HasBeq Key := ⟨Key.beq⟩
 
 inductive Trie (α : Type)
-| node (vs : Array α) (children : Array (Key × Trie)) : Trie
+| node (vs : Array α) (children : Array (Key × Trie α)) : Trie α
 
 end DiscrTree
 
@@ -51,5 +51,4 @@ open Std (PersistentHashMap)
 structure DiscrTree (α : Type) :=
 (root : PersistentHashMap Key (Trie α) := {})
 
-end Meta
-end Lean
+end Lean.Meta