diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index 9cdc501e9..d13f4b904 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -1312,7 +1312,7 @@ class parser::imp {
         }
         updt_options();
         if (m_verbose)
-            regular(m_frontend) << "  Set option: " << id << endl;
+            regular(m_frontend) << "  Set: " << id << endl;
     }
 
     void parse_import() {
diff --git a/tests/lean/arith1.lean.expected.out b/tests/lean/arith1.lean.expected.out
index 8751c4bb4..d6037d1ab 100644
--- a/tests/lean/arith1.lean.expected.out
+++ b/tests/lean/arith1.lean.expected.out
@@ -9,9 +9,9 @@ Int
   Assumed: m
 n + m
 n + x + m
-  Set option: lean::pp::coercion
+  Set: lean::pp::coercion
 (nat_to_int n) + x + (nat_to_int m) + (nat_to_int 10)
 x + (nat_to_int n) + (nat_to_int m) + (nat_to_int 10)
 (nat_to_int (n + m + 10)) + x
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 Int::add (nat_to_int (Nat::add (Nat::add n m) 10)) x
diff --git a/tests/lean/coercion1.lean.expected.out b/tests/lean/coercion1.lean.expected.out
index 49b3fdfac..dcd88cca1 100644
--- a/tests/lean/coercion1.lean.expected.out
+++ b/tests/lean/coercion1.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: T
   Assumed: R
   Assumed: f
diff --git a/tests/lean/coercion2.lean.expected.out b/tests/lean/coercion2.lean.expected.out
index 3f6632fbf..2ef6f55f3 100644
--- a/tests/lean/coercion2.lean.expected.out
+++ b/tests/lean/coercion2.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: T
   Assumed: R
   Assumed: t2r
@@ -9,23 +9,23 @@ g a a
   Assumed: b
 g a b
 g b a
-  Set option: lean::pp::coercion
+  Set: lean::pp::coercion
 g (t2r a) (t2r a)
 g (t2r a) b
 g b (t2r a)
-  Set option: lean::pp::coercion
+  Set: lean::pp::coercion
   Assumed: S
   Assumed: s
   Assumed: r
   Assumed: h
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 g (g a b) a
 h (h r s) r
 R
 S
-  Set option: lean::pp::coercion
+  Set: lean::pp::coercion
 g (g (t2r a) b) (t2r a)
 h (h r s) r
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 (t2r a) ++ b ++ (t2r a)
 r ++ s ++ r
diff --git a/tests/lean/deep.lean.expected.out b/tests/lean/deep.lean.expected.out
index cc164c66c..abaf458e7 100644
--- a/tests/lean/deep.lean.expected.out
+++ b/tests/lean/deep.lean.expected.out
@@ -2,6 +2,6 @@
   Defined: f2
   Defined: f3
   Assumed: f
-  Set option: pp::width
-  Set option: lean::pp::max_depth
+  Set: pp::width
+  Set: lean::pp::max_depth
 f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (…))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out
index 5596fbefd..3636aac18 100644
--- a/tests/lean/ex2.lean.expected.out
+++ b/tests/lean/ex2.lean.expected.out
@@ -1,6 +1,6 @@
-  Set option: pp::colors
+  Set: pp::colors
 ⊤
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 and true false
   Assumed: a
 Error (line: 8, pos: 0) invalid object declaration, environment already has an object named 'a'
@@ -17,5 +17,5 @@ Variable A : Type
 ⟨lean::pp::notation ↦ false, pp::colors ↦ false⟩
 Error (line: 15, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
 Error (line: 16, pos: 23) invalid option value, given option is not an integer
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 a ∧ b
diff --git a/tests/lean/ex3.lean.expected.out b/tests/lean/ex3.lean.expected.out
index 809eb404c..6666bd96b 100644
--- a/tests/lean/ex3.lean.expected.out
+++ b/tests/lean/ex3.lean.expected.out
@@ -9,7 +9,7 @@ expected type
 given type
     T
   Assumed: myeq2
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 Error (line: 9, pos: 15) type mismatch at application argument 3 of
     myeq2::explicit Bool ⊤ a
 expected type
diff --git a/tests/lean/overload1.lean.expected.out b/tests/lean/overload1.lean.expected.out
index 223322518..b2bb13990 100644
--- a/tests/lean/overload1.lean.expected.out
+++ b/tests/lean/overload1.lean.expected.out
@@ -2,7 +2,7 @@
   Assumed: f
   Assumed: g
 ⊤ ++ ⊥ ++ ⊤
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 f (f true false) true
   Assumed: a
   Assumed: b
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index 08ffcc494..f647e85ed 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: N
   Assumed: lt
   Assumed: zero
diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out
index ef7040270..5ad512be1 100644
--- a/tests/lean/tst10.lean.expected.out
+++ b/tests/lean/tst10.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: a
   Assumed: b
 a ∧ b
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 81af0941a..9bd8300b5 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Defined: xor
 ⊤ ⊕ ⊥
 ⊥
diff --git a/tests/lean/tst12.lean.expected.out b/tests/lean/tst12.lean.expected.out
index bf208ff36..44366bbaa 100644
--- a/tests/lean/tst12.lean.expected.out
+++ b/tests/lean/tst12.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
 λ x y : Bool, x ∧ y
 let x := ⊤,
     y := ⊤,
diff --git a/tests/lean/tst13.lean.expected.out b/tests/lean/tst13.lean.expected.out
index 4658987a1..fa6041aea 100644
--- a/tests/lean/tst13.lean.expected.out
+++ b/tests/lean/tst13.lean.expected.out
@@ -1,3 +1,3 @@
-  Set option: pp::colors
+  Set: pp::colors
 λ x x : Bool, x
 let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z
diff --git a/tests/lean/tst14.lean.expected.out b/tests/lean/tst14.lean.expected.out
index e7a0ee738..a7179fc1e 100644
--- a/tests/lean/tst14.lean.expected.out
+++ b/tests/lean/tst14.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
 Int → Int → Int
   Assumed: f
 f 0
diff --git a/tests/lean/tst15.lean.expected.out b/tests/lean/tst15.lean.expected.out
index 5ccd32dda..70c49b085 100644
--- a/tests/lean/tst15.lean.expected.out
+++ b/tests/lean/tst15.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: x
 Type U+3 ⊔ M+2 ⊔ 3
   Assumed: f
diff --git a/tests/lean/tst16.lean.expected.out b/tests/lean/tst16.lean.expected.out
index f9978a85e..e72882484 100644
--- a/tests/lean/tst16.lean.expected.out
+++ b/tests/lean/tst16.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: f
 ∀ a b : Type, (f a) = (f b)
   Assumed: g
diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out
index cf3289bc4..9989c3d24 100644
--- a/tests/lean/tst17.lean.expected.out
+++ b/tests/lean/tst17.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: f
   Assumed: g
 ∀ a b : Type, ∃ c : Type, (g a b) = (f c)
diff --git a/tests/lean/tst2.lean.expected.out b/tests/lean/tst2.lean.expected.out
index f362feaf1..7878b43da 100644
--- a/tests/lean/tst2.lean.expected.out
+++ b/tests/lean/tst2.lean.expected.out
@@ -2,11 +2,11 @@
   Assumed: a
   Assumed: b
 a ∧ b
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 ⟨lean::pp::notation ↦ false⟩
 and a b
 Variable a : Bool
 Variable b : Bool
-  Set option: lean::pp::notation
+  Set: lean::pp::notation
 ⟨lean::pp::notation ↦ true⟩
 a ∧ b
diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out
index 6fd7b4b38..ae0ffe1d4 100644
--- a/tests/lean/tst3.lean.expected.out
+++ b/tests/lean/tst3.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
 Notation 10 if _ then _ : implies
 if ⊤ then ⊥
 if ⊤ then (if a then ⊥)
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index ac27ac3f9..6129bf8f2 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -2,11 +2,11 @@
   Assumed: N
   Assumed: n1
   Assumed: n2
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 f::explicit N n1 n2
 f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
   Assumed: EqNice
-  Set option: pp::colors
+  Set: pp::colors
 EqNice::explicit N n1 n2
 N
 Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b)
diff --git a/tests/lean/tst5.lean.expected.out b/tests/lean/tst5.lean.expected.out
index 481cff1a6..23bb86f6f 100644
--- a/tests/lean/tst5.lean.expected.out
+++ b/tests/lean/tst5.lean.expected.out
@@ -1,10 +1,10 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: N
   Assumed: a
   Assumed: b
 a ≃ b
 Bool
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 heq::explicit N a b
 heq::explicit Type 2 Type 1 Type 1
 heq::explicit Bool ⊤ ⊥
diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out
index 782dd0250..8dc00e7e4 100644
--- a/tests/lean/tst6.lean.expected.out
+++ b/tests/lean/tst6.lean.expected.out
@@ -1,8 +1,8 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: N
   Assumed: h
   Proved: CongrH
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
     Congr::explicit
         N
@@ -15,11 +15,11 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h
         H2
 Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
     CongrH::explicit a1 a2 b1 b2 H1 H2
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2
 Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
   Proved: Example1
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
     DisjCases::explicit
         (a = b ∧ b = c)
@@ -55,7 +55,7 @@ Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
                     (Conjunct2::explicit (a = d) (d = c) H1))
                (Refl::explicit N b))
   Proved: Example2
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
     DisjCases::explicit
         (a = b ∧ b = c)
@@ -91,14 +91,14 @@ Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a
                     (Conjunct2::explicit (a = d) (d = c) H1))
                (Refl::explicit N b))
   Proved: Example3
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
     DisjCases
         H
         (λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
         (λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
   Proved: Example4
-  Set option: lean::pp::implicit
+  Set: lean::pp::implicit
 Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
     DisjCases
         H
diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out
index a6883ba26..0b8acd152 100644
--- a/tests/lean/tst7.lean.expected.out
+++ b/tests/lean/tst7.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
   Assumed: f
 λ (A B : Type) (a : B), f B a
 Error (line: 5, pos: 40) application type mismatch during term elaboration at term
diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out
index 694bdd014..97e3f6559 100644
--- a/tests/lean/tst8.lean.expected.out
+++ b/tests/lean/tst8.lean.expected.out
@@ -1,4 +1,4 @@
-  Set option: pp::colors
+  Set: pp::colors
 Π (A : Type) (a : A), A
   Assumed: g
   Defined: f