diff --git a/src/main/isabelle/Leon_Library.thy b/src/main/isabelle/Leon_Library.thy
index 62d7108d45ecd4371b450e5b2ba123292647d687..4327381f8b44ca5855f23aa86e9e9af689409a60 100644
--- a/src/main/isabelle/Leon_Library.thy
+++ b/src/main/isabelle/Leon_Library.thy
@@ -5,6 +5,8 @@ begin
 axiomatization
   error :: "nat \<Rightarrow> 'a"
 
+typedecl string
+
 declare [[code abort: error]]
 
 declare null_rec[simp]
diff --git a/src/main/scala/leon/solvers/isabelle/Types.scala b/src/main/scala/leon/solvers/isabelle/Types.scala
index 0e609155104023776b5c53934db9cc15cb09c811..7d2b4d1d8d54667343ae8e6d6a458130c5baef13 100644
--- a/src/main/scala/leon/solvers/isabelle/Types.scala
+++ b/src/main/scala/leon/solvers/isabelle/Types.scala
@@ -127,6 +127,9 @@ final class Types(context: LeonContext, program: Program, system: System)(implic
             case Some(datatype) => datatype.typ
           }}.map { Type(_, args) }
         }
+      case StringType =>
+        context.reporter.warning("Strings are not yet supported, translating to unspecified type")
+        Future.successful { Type("Leon_Library.string", Nil) }
       case _ if strict =>
         context.reporter.fatalError(s"Unsupported type $tree, can't be inferred")
       case _ =>