diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
index e03d3889d..14f22cbab 100644
--- a/library/data/finset/comb.lean
+++ b/library/data/finset/comb.lean
@@ -351,7 +351,7 @@ quot.lift_on₂ s₁ s₂
   (λ l₁ l₂,
     to_finset_of_nodup (product (elt_of l₁) (elt_of l₂))
                        (nodup_product (has_property l₁) (has_property l₂)))
-  (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_product p₁ p₂))
+  (λ v₁ v₂ w₁ w₂ p₁ p₂, begin apply @quot.sound, apply perm_product p₁ p₂ end)
 
 infix [priority finset.prio] * := product
 
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 44d24630f..c85a0a2b5 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -48,10 +48,12 @@ attribute int.of_nat [coercion]
 
 notation `-[1+ ` n `]` := int.neg_succ_of_nat n    -- for pretty-printing output
 
-definition int_has_zero [reducible] [instance] : has_zero int :=
+protected definition prio : num := num.pred nat.prio
+
+definition int_has_zero [reducible] [instance] [priority int.prio] : has_zero int :=
 has_zero.mk (of_nat 0)
 
-definition int_has_one [reducible] [instance] : has_one int :=
+definition int_has_one [reducible] [instance] [priority int.prio] : has_one int :=
 has_one.mk (of_nat 1)
 
 theorem of_nat_zero : of_nat (0:nat) = (0:int) :=
@@ -89,8 +91,6 @@ protected definition mul : ℤ → ℤ → ℤ
 
 /- notation -/
 
-protected definition prio : num := num.pred nat.prio
-
 definition int_has_add [reducible] [instance] [priority int.prio] : has_add int := has_add.mk int.add
 definition int_has_neg [reducible] [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
 definition int_has_mul [reducible] [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul