From cc87ca9e52ece7d70f81efb1838be77151463b03 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 30 Oct 2012 16:45:52 +0100
Subject: [PATCH] Always rely on CaseClassPattern, not InstanceOfPattern

---
 src/main/scala/leon/purescala/TreeOps.scala | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index e6b09cc17..8baa7e8dc 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1159,12 +1159,7 @@ object TreeOps {
               }
             }
 
-            if (subconds.forall(_.isInstanceOf[WildcardPattern])) {
-              // nothing to check underneath
-              InstanceOfPattern(Some(binder), cd)
-            } else {
-              CaseClassPattern(Some(binder), cd, subconds)
-            }
+            CaseClassPattern(Some(binder), cd, subconds)
           }
 
           val (scrutinees, patterns) = scrutSet.toSeq.map(s => (s, computePatternFor(conditions(s), s))) unzip
-- 
GitLab