diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index fbe78e49a..9c0cad91e 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -35,8 +35,14 @@ refl : eq a a
 inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
 refl : heq a a
 
-structure prod (A B : Type) :=
-mk :: (pr1 : A) (pr2 : B)
+inductive prod (A B : Type) :=
+mk : A → B → prod A B
+
+definition prod.pr1 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : A :=
+prod.rec (λ a b, a) p
+
+definition prod.pr2 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : B :=
+prod.rec (λ a b, b) p
 
 inductive and (a b : Prop) : Prop :=
 intro : a → b → and a b
diff --git a/library/init/prod.lean b/library/init/prod.lean
index 34e7ca7be..a2a95c965 100644
--- a/library/init/prod.lean
+++ b/library/init/prod.lean
@@ -27,6 +27,16 @@ namespace prod
   postfix `.2`:(max+1) := pr2
   end ops
 
+  definition destruct [reducible] := @prod.cases_on
+
+  section
+  variables {A B : Type}
+  lemma pr1.mk (a : A) (b : B) : pr1 (mk a b) = a := rfl
+  lemma pr2.mk (a : A) (b : B) : pr2 (mk a b) = b := rfl
+  lemma eta : ∀ (p : A × B), mk (pr1 p) (pr2 p) = p
+  | (a, b) := rfl
+  end
+
   open well_founded
 
   section
diff --git a/tests/lean/630.lean.expected.out b/tests/lean/630.lean.expected.out
index 764d2703b..83f80820b 100644
--- a/tests/lean/630.lean.expected.out
+++ b/tests/lean/630.lean.expected.out
@@ -1,7 +1,6 @@
 inductive pnat.pnat : Type₁
 constructors:
 pnat.pnat.pos : Π (n : ℕ), nat.gt n (nat.of_num 0) → ℕ+
-structure prod : Type → Type → Type
-fields:
-prod.pr1 : Π {A : Type} {B : Type}, A × B → A
-prod.pr2 : Π {A : Type} {B : Type}, A × B → B
+inductive prod : Type → Type → Type
+constructors:
+prod.mk : Π {A : Type} {B : Type}, A → B → A × B
diff --git a/tests/lean/run/struct_inst_exprs.lean b/tests/lean/run/struct_inst_exprs.lean
index e95e1bb6e..36b310924 100644
--- a/tests/lean/run/struct_inst_exprs.lean
+++ b/tests/lean/run/struct_inst_exprs.lean
@@ -2,7 +2,7 @@ open nat prod
 
 set_option pp.coercions true
 
-definition s : nat × nat := {| prod, pr1 := 10, pr2 := 20 |}
+definition s : nat × nat := pair 10 20
 
 structure test :=
 (A : Type) (a : A) (B : A → Type) (b : B a)