From ae7c8f407079b0a7c24cc5fc310ebff8c51ec52b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 31 Dec 2016 15:19:58 +0100
Subject: [PATCH] fix(shell/lean_js): the and_comm name is taken now

---
 src/shell/lean_js.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/shell/lean_js.html b/src/shell/lean_js.html
index be9938eee8..76251d7973 100644
--- a/src/shell/lean_js.html
+++ b/src/shell/lean_js.html
@@ -58,7 +58,7 @@ outputLog('--- Import complete. ' + checkTimer());
 outputLog('--- Writing test.lean to virtual FS...'); startTimer();
 testfile = ''
          + 'variables p q r s : Prop\n'
-         + 'theorem and_comm : p ∧ q ↔ q ∧ p :=\n'
+         + 'theorem my_and_comm : p ∧ q ↔ q ∧ p :=\n'
          + 'iff.intro\n'
          + '  (assume Hpq : p ∧ q,\n'
          + '    and.intro (and.elim_right Hpq) (and.elim_left Hpq))\n'