# HG changeset patch
# User wenzelm
# Date 1478551961 -3600
# Node ID d751bef76e5c612b24057c9afb6e9396cb28b346
# Parent  d072c8169c7caa4e1cee79cc360648569c071774
tuned;

diff -r d072c8169c7c -r d751bef76e5c src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Mon Nov 07 21:40:43 2016 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Mon Nov 07 21:52:41 2016 +0100
@@ -300,7 +300,7 @@
 
 theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
-  assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
+  assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
   show A
   proof (rule classical)
     assume "\<not> A"
@@ -309,7 +309,7 @@
       assume A
       with \<open>\<not> A\<close> show B by (rule contradiction)
     qed
-    with a show A ..
+    with * show A ..
   qed
 qed