diff --git a/src/main/scala/leon/purescala/SubTreeOps.scala b/src/main/scala/leon/purescala/SubTreeOps.scala
index 1d96f070b1538a1a4d40a9e845d215dbf4848d77..39ed1a45509648ed5bdc26b92f5006d815f8f941 100644
--- a/src/main/scala/leon/purescala/SubTreeOps.scala
+++ b/src/main/scala/leon/purescala/SubTreeOps.scala
@@ -276,6 +276,19 @@ trait SubTreeOps[SubTree <: Tree]  {
     rec(e, c)
   }
 
+  def preFoldWithContext[C](f: (SubTree, C) => C, combiner: (SubTree, C, Seq[C]) => C)
+                           (e: SubTree, c: C): C = {
+
+    def rec(eIn: SubTree, cIn: C): C = {
+      val ctx = f(eIn, cIn)
+      val Deconstructor(es, _) = eIn
+      val cs = es.map{ rec(_, ctx) }
+      combiner(eIn, ctx, cs)
+    }
+
+    rec(e, c)
+  }
+
   /*
    * =============
    * Auxiliary API
@@ -322,4 +335,4 @@ trait SubTreeOps[SubTree <: Tree]  {
     res
   }
 
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index b461a51c64d28a4f589f7182f4342ee58d08ddbd..0ee936c813b942d3e55564506a200b31630f0283 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -98,7 +98,7 @@ object Types {
 
     assert(classDef.tparams.size == tps.size)
 
-    def fields = {
+    lazy val fields = {
       val tmap = (classDef.tparams zip tps).toMap
       if (tmap.isEmpty) {
         classDef.fields