diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean
index 6f10c4eb76..b10bb576af 100644
--- a/src/Lean/Data/PrefixTree.lean
+++ b/src/Lean/Data/PrefixTree.lean
@@ -64,7 +64,7 @@ partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α
       | some t => find ks t d
   find k t init
 
-inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
+inductive WellFormed {β} (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
   | emptyWff    : WellFormed cmp empty
   | insertWff  {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed cmp t → WellFormed cmp (insert t cmp k val)