diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean
index d0e96aa62506..c7c6b48cec35 100644
--- a/src/Lean/Meta/DiscrTreeTypes.lean
+++ b/src/Lean/Meta/DiscrTreeTypes.lean
@@ -26,13 +26,13 @@ inductive Key where
   deriving Inhabited, BEq, Repr
 
 protected def Key.hash : Key → UInt64
-  | .const n a   => mixHash 5237 $ mixHash (hash n) (hash a)
+  | .const n a   => mixHash (hash n) (hash a)
   | .fvar n a    => mixHash 3541 $ mixHash (hash n) (hash a)
   | .lit v       => mixHash 1879 $ hash v
   | .star        => 7883
   | .other       => 2411
   | .arrow       => 17
-  | .proj s i a  =>  mixHash (hash a) $ mixHash (hash s) (hash i)
+  | .proj s i a  =>  mixHash 5237 $ mixHash (hash a) $ mixHash (hash s) (hash i)
 
 instance : Hashable Key := ⟨Key.hash⟩
 
diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean
index 29a37cdd8218..22b69959cf95 100644
--- a/src/Lean/Meta/LazyDiscrTree.lean
+++ b/src/Lean/Meta/LazyDiscrTree.lean
@@ -42,13 +42,13 @@ namespace Key
 
 /-- Hash function -/
 protected def hash : Key → UInt64
-  | .const n a   => mixHash 5237 $ mixHash n.hash (hash a)
+  | .const n a   => mixHash (hash n) (hash a)
   | .fvar n a    => mixHash 3541 $ mixHash (hash n) (hash a)
   | .lit v       => mixHash 1879 $ hash v
   | .star        => 7883
   | .other       => 2411
   | .arrow       => 17
-  | .proj s i a  =>  mixHash (hash a) $ mixHash (hash s) (hash i)
+  | .proj s i a  => mixHash 5237 $ mixHash (hash a) $ mixHash (hash s) (hash i)
 
 instance : Hashable Key := ⟨Key.hash⟩