diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 998a1be177867202218f511a0d0af3a23083ef72..49e17e4416d38d53a8f5ab7a24d01fff67c0fd57 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -3,6 +3,7 @@ package synthesis
 
 import purescala.TreeOps.simplifyLets
 import purescala.Trees.Expr
+import purescala.ScalaPrinter
 import purescala.Definitions.Program
 
 object SynthesisPhase extends LeonPhase[Program, Program] {
@@ -46,6 +47,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       for (file <- ctx.files) {
         new FileInterface(ctx.reporter, file).updateFile(chooseToExprs)
       }
+    } else {
+      for ((chs, ex) <- chooseToExprs) {
+        ctx.reporter.info("-"*80)
+        ctx.reporter.info("For: "+chs)
+        ctx.reporter.info("Synthesized Code:\n"+ScalaPrinter(ex))
+      }
     }
 
     p
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 741915babfe6c87f4565ebdbda8b7467479d1eac..0dc4cb283f48c0674b8a3638a1e4f875f7e9affc 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -110,18 +110,10 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
         val as = (variablesOf(pred)--xs).toList
         val phi = pred
 
-        info("")
-        info("")
-        info("In Function "+f.id+":")
-        info("-"*80)
-
         val sol = synthesize(Problem(as, phi, xs), rules)
 
         solutions += ch -> sol
 
-        info("Scala code:")
-        info(ScalaPrinter(simplifyLets(sol.toExpr)))
-
         a
       case _ =>
         a