From 753d5d0689f9d89ceab38f7060f5514b340220cd Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 21 Jan 2016 17:09:34 -0800 Subject: [PATCH] fix(library/blast/grind/intro_elim_lemmas): need to copy expr --- src/library/blast/grinder/intro_elim_lemmas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/blast/grinder/intro_elim_lemmas.cpp b/src/library/blast/grinder/intro_elim_lemmas.cpp index 3365cd39f..ee9582621 100644 --- a/src/library/blast/grinder/intro_elim_lemmas.cpp +++ b/src/library/blast/grinder/intro_elim_lemmas.cpp @@ -82,7 +82,7 @@ optional get_intro_target(tmp_type_context & ctx, name const & c) { expr local = ctx.mk_tmp_local(binding_domain(type)); type = ctx.try_to_pi(instantiate(binding_body(type), local)); } - expr const & fn = get_app_fn(ctx.whnf(type)); + expr const fn = get_app_fn(ctx.whnf(type)); if (is_constant(fn)) return optional(const_name(fn)); else