diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 9ae497e6c7585bb1b3527e25c659d82cf5f5d5dd..6f5d2aff477af4e27369bb790f3d58084b3802f6 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -79,11 +79,7 @@ object Trees {
   case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
     val fixedType = funDef.returnType
 
-    funDef.args.zip(args).foreach{ case (a, c) =>
-      if (!isSubtypeOf(c.getType, a.tpe)) {
-        throw new TypeErrorException("Invalid invocation of "+funDef.id+": argument "+a.id+":"+a.tpe+" was passed "+c+":"+c.getType)
-      }
-    }
+    funDef.args.zip(args).foreach{ case (a, c) => typeCheck(c, a.tpe) }
   }
   case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr