From 17a2f1fe472bfd2a5a96ad465c0e2dfb29b84831 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Jan 2016 16:46:15 -0800
Subject: [PATCH] chore(tests/lean/run/blast_grind1): use 'core_grind'

Reason: we will change the semantics of 'grind'
---
 tests/lean/run/blast_grind1.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/blast_grind1.lean b/tests/lean/run/blast_grind1.lean
index 08c382c106..54fe83b08f 100644
--- a/tests/lean/run/blast_grind1.lean
+++ b/tests/lean/run/blast_grind1.lean
@@ -11,12 +11,12 @@ by blast
 
 print ex1
 
-attribute Exists.intro [intro!] -- grind and core_grind only process [intro!] declarations
+attribute Exists.intro [intro!] -- core_grind only process [intro!] declarations
 
 example (p q : nat → Prop) : (∃ x, p x ∧ q x) → (∃ x, q x) ∧ (∃ x, p x) :=
 by blast
 
-set_option blast.strategy "grind"
+set_option blast.strategy "core_grind"
 
 example (a b c : nat) : a = b ∨ a = c → b = c → b = a :=
 by blast