From 34ff60de0ab0a05c85e6af50ed6d1a93805e040b Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 23 Jul 2013 10:28:04 -0700
Subject: Did some refactoring.

---
 Source/VCExpr/TypeErasure.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/VCExpr/TypeErasure.cs')

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 9614f9f8..4111c9df 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1362,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure {
       List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, newPolarity);
       Type/*!*/ oldType = node[0].Type;
       if (AxBuilder.UnchangedType(oldType) &&
-          node.All(e => e.Type.Equals(oldType)))
+          node.Skip(1).All(e => e.Type.Equals(oldType)))
         return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));
       else
         return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));
-- 
cgit v1.2.3