diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 6952542d69466485806a4bf564d9608c9e746aa8..b36b2e1cca7dba821975e1ae4dd3e0b9ccef4208 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -609,7 +609,7 @@ class PrettyPrinter(opts: PrinterOptions,
     case (_: Modulo) => 1
     case (_: Or | BinaryMethodCall(_, "||", _)) => 2
     case (_: And | BinaryMethodCall(_, "&&", _)) => 3
-    case (_: GreaterThan | _: GreaterEquals  | _: LessEquals | _: LessThan) => 4
+    case (_: GreaterThan | _: GreaterEquals  | _: LessEquals | _: LessThan | _: Implies) => 4
     case (_: Equals | _: Not) => 5
     case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 7
     case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Remainder | _: BVRemainder | BinaryMethodCall(_, "*" | "/", _)) => 8
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 979ccd38c0f653f0b29214b44f6da1d7da44bc12..5fd883b94507640dfedd799f758aef39cb3c5cd6 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -25,17 +25,16 @@ class ScalaPrinter(opts: PrinterOptions,
           case f: FunDef if f.isSynthetic => false
           case _ => true
         }))
-      case Not(Equals(l, r))         => p"$l != $r"
-      case Implies(l,r)              => p"$l ==> $r"
+      case Not(Equals(l, r))         => optP { p"$l != $r" }
       case Choose(pred)              => p"choose($pred)"
       case s @ FiniteSet(rss, t)     => p"Set[$t](${rss.toSeq})"
       case m @ FiniteMap(els, k, v)  => p"Map[$k,$v]($els)"
       
       case ElementOfSet(e,s)         => p"$s.contains(e)"
-      case SetUnion(l,r)             => p"$l ++ $r"
-      case MapUnion(l,r)             => p"$l ++ $r"
-      case SetDifference(l,r)        => p"$l -- $r"
-      case SetIntersection(l,r)      => p"$l & $r"
+      case SetUnion(l,r)             => optP { p"$l ++ $r" }
+      case MapUnion(l,r)             => optP { p"$l ++ $r" }
+      case SetDifference(l,r)        => optP { p"$l -- $r" }
+      case SetIntersection(l,r)      => optP { p"$l & $r" }
       case SetCardinality(s)         => p"$s.size"
       case InfiniteIntegerLiteral(v) => p"BigInt($v)"