diff -r 4320875eb8a1 -r ee2c7f0dd1be src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/HOL/HOL.thy	Fri Jun 19 09:46:47 2020 +0000
@@ -943,32 +943,34 @@
 
 lemma subst_all:
   \<open>(\<And>x. x = a \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close>
-proof (rule equal_intr_rule)
-  assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P x\<close>
-  show \<open>PROP P a\<close>
-    by (rule *) (rule refl)
-next
-  fix x
-  assume \<open>PROP P a\<close> and \<open>x = a\<close>
-  from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
-    by (rule eq_reflection)
-  with \<open>PROP P a\<close> show \<open>PROP P x\<close>
-    by simp
-qed
-
-lemma subst_all':
   \<open>(\<And>x. a = x \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close>
-proof (rule equal_intr_rule)
-  assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P x\<close>
-  show \<open>PROP P a\<close>
-    by (rule *) (rule refl)
-next
-  fix x
-  assume \<open>PROP P a\<close> and \<open>a = x\<close>
-  from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
-    by (rule eq_reflection)
-  with \<open>PROP P a\<close> show \<open>PROP P x\<close>
-    by simp
+proof -
+  show \<open>(\<And>x. x = a \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close>
+  proof (rule equal_intr_rule)
+    assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P x\<close>
+    show \<open>PROP P a\<close>
+      by (rule *) (rule refl)
+  next
+    fix x
+    assume \<open>PROP P a\<close> and \<open>x = a\<close>
+    from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
+      by (rule eq_reflection)
+    with \<open>PROP P a\<close> show \<open>PROP P x\<close>
+      by simp
+  qed
+  show \<open>(\<And>x. a = x \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close>
+  proof (rule equal_intr_rule)
+    assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P x\<close>
+    show \<open>PROP P a\<close>
+      by (rule *) (rule refl)
+  next
+    fix x
+    assume \<open>PROP P a\<close> and \<open>a = x\<close>
+    from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
+      by (rule eq_reflection)
+    with \<open>PROP P a\<close> show \<open>PROP P x\<close>
+      by simp
+  qed
 qed
 
 lemma simp_thms:
@@ -1403,7 +1405,6 @@
   all_simps
   simp_thms
   subst_all
-  subst_all'
 
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = if_split