diff --git a/theories/infinite.v b/theories/infinite.v
index c31d73ac0fc41d24117f31e533d8b13f5573a6f0..23767b8371a0a32d8eb31f7a72f3d7204d4eb59b 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -71,7 +71,7 @@ Section Fresh.
       apply inbelow; omega.
   Qed.
 
-  Instance fresh_generic: Fresh A C | 20 := λ s, fresh_generic_fix (1 + Nat.log2 (size s)) s 0.
+  Instance fresh_generic: Fresh A C := λ s, fresh_generic_fix s 0.
 
   Instance fresh_generic_spec: FreshSpec A C.
   Proof.