diff --git a/library/init/core.lean b/library/init/core.lean
index 92952c544b..301663126f 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -254,8 +254,8 @@ class has_ssubset  (α : Type u) := (ssubset : α → α → Prop)
 class has_emptyc   (α : Type u) := (emptyc : α)
 class has_insert   (α : out_param (Type u)) (γ : Type v) := (insert : α → γ → γ)
 /- Type class used to implement the notation { a ∈ c | p a } -/
-class has_sep (α : Type u) (γ : Type u → Type v) :=
-(sep : (α → Prop) → γ α → γ α)
+class has_sep (α : out_param (Type u)) (γ : Type v) :=
+(sep : (α → Prop) → γ → γ)
 /- Type class for set-like membership -/
 class has_mem (α : out_param (Type u)) (γ : Type v) := (mem : α → γ → Prop)
 
@@ -301,7 +301,7 @@ has_emptyc.emptyc α
 def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
 insert a emptyc
 
-def sep {α : Type u} {γ : Type u → Type v} [has_sep α γ] : (α → Prop) → γ α → γ α :=
+def sep {α : Type u} {γ : Type v} [has_sep α γ] : (α → Prop) → γ → γ :=
 has_sep.sep
 
 def mem {α : Type u} {γ : Type v} [has_mem α γ] : α → γ → Prop :=
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index d445c885c1..f10af71c1d 100644
--- a/library/init/data/set.lean
+++ b/library/init/data/set.lean
@@ -30,7 +30,7 @@ instance : has_subset (set α) :=
 protected def sep (p : α → Prop) (s : set α) : set α :=
 {a | a ∈ s ∧ p a}
 
-instance : has_sep α set :=
+instance : has_sep α (set α) :=
 ⟨set.sep⟩
 
 instance : has_emptyc (set α) :=
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index 78577f9272..b3c8209f8a 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -16,7 +16,7 @@ has_mul : Type u → Type u
 has_neg : Type u → Type u
 has_one : Type u → Type u
 has_sdiff : Type u → Type u
-has_sep : Type u → (Type u → Type v) → Type (max u v)
+has_sep : out_param Type u → Type v → Type (max u v)
 has_sizeof : Sort u → Sort (max 1 u)
 has_ssubset : Type u → Type u
 has_sub : Type u → Type u
@@ -42,7 +42,7 @@ has_mul : Type u → Type u
 has_neg : Type u → Type u
 has_one : Type u → Type u
 has_sdiff : Type u → Type u
-has_sep : Type u → (Type u → Type v) → Type (max u v)
+has_sep : out_param Type u → Type v → Type (max u v)
 has_sizeof : Sort u → Sort (max 1 u)
 has_ssubset : Type u → Type u
 has_sub : Type u → Type u