From 4781fc8365293dccf9efb4647129f283dc81567b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Jan 2015 22:20:08 -0800
Subject: [PATCH] fix(library/init/logic): eq.symm should not use eq.subst

Reason: eq.symm is used by definitional package, and eq.subst is opaque.
Thus, computation will get stuck if it depends on eq.subst.
---
 library/init/logic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/logic.lean b/library/init/logic.lean
index 074a760a3..7549c82ae 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -43,7 +43,7 @@ namespace eq
   subst H₂ H₁
 
   definition symm (H : a = b) : b = a :=
-  subst H (refl a)
+  rec (refl a) H
 
   namespace ops
     notation H `⁻¹` := symm H --input with \sy or \-1 or \inv