diff -r 8d0294d877bd -r 107941e8fa01 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 28 22:14:44 2021 +0200
@@ -888,7 +888,7 @@
   structure Blast = Blast
   (
     structure Classical = Classical
-    val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
+    val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close>
     val equality_name = \<^const_name>\<open>HOL.eq\<close>
     val not_name = \<^const_name>\<open>Not\<close>
     val notE = @{thm notE}
@@ -1549,7 +1549,7 @@
         {lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
-            _ $ (P as _ $ \<^const>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
+            _ $ (P as _ $ \<^Const_>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
               if P <> Q then SOME Drule.swap_prems_eq else NONE
           | _ => NONE)},
        Simplifier.make_simproc \<^context> "induct_equal_conj_curry"
@@ -1558,11 +1558,11 @@
           (case Thm.term_of ct of
             _ $ (_ $ P) $ _ =>
               let
-                fun is_conj (\<^const>\<open>induct_conj\<close> $ P $ Q) =
+                fun is_conj \<^Const_>\<open>induct_conj for P Q\<close> =
                       is_conj P andalso is_conj Q
-                  | is_conj (Const (\<^const_name>\<open>induct_equal\<close>, _) $ _ $ _) = true
-                  | is_conj \<^const>\<open>induct_true\<close> = true
-                  | is_conj \<^const>\<open>induct_false\<close> = true
+                  | is_conj \<^Const_>\<open>induct_equal _ for _ _\<close> = true
+                  | is_conj \<^Const_>\<open>induct_true\<close> = true
+                  | is_conj \<^Const_>\<open>induct_false\<close> = true
                   | is_conj _ = false
               in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
             | _ => NONE)}]