diff --git a/library/data/prod/default.lean b/library/data/prod/default.lean
index 560debabf5..d3e25a6d4f 100644
--- a/library/data/prod/default.lean
+++ b/library/data/prod/default.lean
@@ -1,4 +1,4 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
-import data.prod.decl data.prod.thms
+import data.prod.decl data.prod.thms data.prod.wf
diff --git a/library/data/prod/wf.lean b/library/data/prod/wf.lean
index 74caa05ee3..d91c736ed0 100644
--- a/library/data/prod/wf.lean
+++ b/library/data/prod/wf.lean
@@ -50,13 +50,6 @@ namespace prod
   definition lex.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) :=
   well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) (well_founded.apply Hb) b))
 
-  end
-
-  context
-  parameters {A B : Type}
-  parameters {Ra  : A → A → Prop} {Rb  : B → B → Prop}
-  infix `≺`:50 := rprod Ra Rb
-
   -- Relational product is a subrelation of the lex
   definition rprod.sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b :=
   λa b H, rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁)
diff --git a/library/data/sigma/default.lean b/library/data/sigma/default.lean
index 53f2d09ea5..ae9f0b096e 100644
--- a/library/data/sigma/default.lean
+++ b/library/data/sigma/default.lean
@@ -1,4 +1,4 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-import data.sigma.decl data.sigma.thms
+import data.sigma.decl data.sigma.thms data.sigma.wf