From 9d37f53d8393469cb33fb8ad4b07d21eef79a0ac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Aug 2019 09:46:44 -0700
Subject: [PATCH] fix(tests/lean/run/new_compiler): broken test

---
 tests/lean/run/new_compiler.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/new_compiler.lean b/tests/lean/run/new_compiler.lean
index 2e41263a49..92c532e7ad 100644
--- a/tests/lean/run/new_compiler.lean
+++ b/tests/lean/run/new_compiler.lean
@@ -41,8 +41,10 @@ def add' : Nat → Nat → Nat
 def aux (i : Nat) (h : i > 0) :=
 i
 
+axiom bad (α : Sort u) : α
+
 unsafe def foo2 : Nat :=
-@False.rec (fun _ => Nat) sorry
+@False.rec (fun _ => Nat) (bad _)
 
 set_option pp.notation false