--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Sep 28 22:08:51 2021 +0200
@@ -76,17 +76,17 @@
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
fun do_formula pos t =
(case (pos, t) of
- (_, \<^const>\<open>Trueprop\<close> $ t1) => do_formula pos t1
+ (_, \<^Const_>\<open>Trueprop for t1\<close>) => do_formula pos t1
| (true, Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
| (true, Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
| (false, Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
- | (_, \<^const>\<open>Pure.imp\<close> $ t1 $ t2) =>
+ | (_, \<^Const_>\<open>Pure.imp for t1 t2\<close>) =>
do_formula (not pos) t1 andalso (t2 = \<^prop>\<open>False\<close> orelse do_formula pos t2)
- | (_, \<^const>\<open>HOL.implies\<close> $ t1 $ t2) =>
- do_formula (not pos) t1 andalso (t2 = \<^const>\<open>False\<close> orelse do_formula pos t2)
- | (_, \<^const>\<open>Not\<close> $ t1) => do_formula (not pos) t1
- | (true, \<^const>\<open>HOL.disj\<close> $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (false, \<^const>\<open>HOL.conj\<close> $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (_, \<^Const_>\<open>implies for t1 t2\<close>) =>
+ do_formula (not pos) t1 andalso (t2 = \<^Const>\<open>False\<close> orelse do_formula pos t2)
+ | (_, \<^Const_>\<open>Not for t1\<close>) => do_formula (not pos) t1
+ | (true, \<^Const_>\<open>disj for t1 t2\<close>) => forall (do_formula pos) [t1, t2]
+ | (false, \<^Const_>\<open>conj for t1 t2\<close>) => forall (do_formula pos) [t1, t2]
| (true, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2
| (true, Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2
| _ => false)