diff --git a/source/pervasive/relations.rs b/source/pervasive/relations.rs
index 194078be01..7d2190b376 100644
--- a/source/pervasive/relations.rs
+++ b/source/pervasive/relations.rs
@@ -135,10 +135,4 @@ verus! {
             } ;
         }
     }
-
-    pub open spec fn merge_sort_by<A>(s: Seq<A>, leq: FnSpec(A,A) -> bool) -> Seq<A>
-    {
-        s
-    }
-
 }
\ No newline at end of file