diff --git a/library/collection/List.scala b/library/collection/List.scala
index 436886cca2d4c7893092730151c3648f24569b24..74a0f0c66e3bc23780076e16acdc6f7035c6986b 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -673,14 +673,13 @@ object ListSpecs {
   def headReverseLast[T](l: List[T]): Boolean = {
     require (!l.isEmpty)
     (l.head == l.reverse.last) because {
-      l match {
-        case Cons(x, xs) => {
-          (x :: xs).head           ==| trivial                 |
-          x                        ==| snocLast(xs.reverse, x) |
-          (xs.reverse :+ x).last   ==| trivial                 |
-          (x :: xs).reverse.last
-        }.qed
-      }
+      val Cons(x, xs) = l;
+      {
+        (x :: xs).head           ==| trivial                 |
+        x                        ==| snocLast(xs.reverse, x) |
+        (xs.reverse :+ x).last   ==| trivial                 |
+        (x :: xs).reverse.last
+      }.qed
     }
   }.holds