From 2606021304e2b2d2a977e95267f35159c551e31c Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 20 Dec 2022 16:51:02 -0800
Subject: [PATCH] fix: use ppTerm instead of formatTerm

---
 tests/lean/formatTerm.lean              |  2 +-
 tests/lean/formatTerm.lean.expected.out | 66 ++++++++++++-------------
 2 files changed, 34 insertions(+), 34 deletions(-)

diff --git a/tests/lean/formatTerm.lean b/tests/lean/formatTerm.lean
index be285eb6d7..d4a8185855 100644
--- a/tests/lean/formatTerm.lean
+++ b/tests/lean/formatTerm.lean
@@ -1,7 +1,7 @@
 import Lean
 open Lean PrettyPrinter
 
-def fmt (stx : CoreM Syntax) : CoreM Format := stx >>= formatTerm
+def fmt (stx : CoreM Syntax) : CoreM Format := do PrettyPrinter.ppTerm ⟨← stx⟩
 
 #eval fmt `(if c then do t else e)
 #eval fmt `(if c then do t; t else e)
diff --git a/tests/lean/formatTerm.lean.expected.out b/tests/lean/formatTerm.lean.expected.out
index f62a00c9b3..c4c162919d 100644
--- a/tests/lean/formatTerm.lean.expected.out
+++ b/tests/lean/formatTerm.lean.expected.out
@@ -1,38 +1,38 @@
-if c.1 then do
-  t.1
-else e.1
-if c.1 then do
-  t.1;
-  t.1
-else e.1
-if c.1 then do
-  t.1
+if c✝ then do
+  t✝
+else e✝
+if c✝ then do
+  t✝;
+  t✝
+else e✝
+if c✝ then do
+  t✝
 else do
-  e.1
-if let x.1 := c.1 then do
-  t.1
+  e✝
+if let x✝ := c✝ then do
+  t✝
 else do
-  e.1
-if c.1 then do
-  t.1
+  e✝
+if c✝ then do
+  t✝
 else
-  if c.1 then do
-    t.1
+  if c✝ then do
+    t✝
   else do
-    e.1
+    e✝
 do
-  if c.1 then 
-    t.1
+  if c✝ then 
+    t✝
   else
-    e.1
+    e✝
 do
-  if c.1 then 
-    t.1
-  else if c.1 then
-    t.1
+  if c✝ then 
+    t✝
+  else if c✝ then
+    t✝
   else
-    e.1
-def foo.1 := by 
+    e✝
+def foo✝ := by 
   · skip; skip
   · skip; skip
     skip
@@ -56,9 +56,9 @@ by try  skip
 by  try skip
         skip
     skip
-{ foo.1 := bar.1
-  bar.1 := foo.1 + bar.1 }
-let x.1 :=
-  { foo.1 := bar.1
-    bar.1 := foo.1 + bar.1 }
-x.1
+{ foo✝ := bar✝
+  bar✝ := foo✝ + bar✝ }
+let x✝ :=
+  { foo✝ := bar✝
+    bar✝ := foo✝ + bar✝ }
+x✝