diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 8d7677d3235364009e17b5438d9742efeafe9cf2..903d9e25f8650fd607c6784a0a63d4b142a7822b 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -67,10 +67,13 @@ object Problem {
     eb: ExamplesBank = ExamplesBank.empty,
     fd: Option[FunDef] = None
   ): Problem = {
-    val xs = {
-      val tps = spec.getType.asInstanceOf[FunctionType].from
-      tps map (FreshIdentifier("x", _, alwaysShowUniqueID = true))
-    }.toList
+    val xs = (spec match {
+      case Lambda(args, _) => args.map(_.id)
+      case IsTyped(_, FunctionType(from, to)) =>
+        from map (FreshIdentifier("x", _, alwaysShowUniqueID = true))
+      case _ =>
+        throw LeonFatalError(s"$spec is the spec of a choose but is not a function?")
+    }).toList
 
     val phi = application(simplifyLets(spec), xs map { _.toVariable})
     val as = (variablesOf(phi) ++ pc.variables -- xs).toList.sortBy(_.name)