From 8ee1d35bed165103c90583b0ae548673ee4822c0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jul 2015 12:51:42 -0700
Subject: [PATCH] fix(tests/lean/unfold_crash): fixed regression test for bug
 reported by Rob

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

diff --git a/tests/lean/unfold_crash.lean b/tests/lean/unfold_crash.lean
index edfc48e9f..45329abfa 100644
--- a/tests/lean/unfold_crash.lean
+++ b/tests/lean/unfold_crash.lean
@@ -4,6 +4,6 @@ open nat
 example (a b : nat) : a = succ b → a = b + 1 :=
 begin
   intro h,
-  try (unfold succ at h)
+  try (unfold succ at h),
   unfold succ at h
 end
diff --git a/tests/lean/unfold_crash.lean.expected.out b/tests/lean/unfold_crash.lean.expected.out
index 1e2d2e56d..750468112 100644
--- a/tests/lean/unfold_crash.lean.expected.out
+++ b/tests/lean/unfold_crash.lean.expected.out
@@ -1 +1 @@
-unfold_crash.lean:8:2: error: invalid 'begin-end' expression, ',' expected
+unfold_crash.lean:8:9: error: invalid 'unfold', 'nat.succ' is not a definition