--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Aug 04 17:39:47 2024 +0200
@@ -555,13 +555,12 @@
val (h, args) =
strip_comb t'
|> apfst (strip_abs #> snd #> strip_comb #> fst)
- val get_const_name = dest_Const #> fst
val h_property =
is_Free h orelse
is_Var h orelse
(is_Const h
- andalso (get_const_name h <> get_const_name \<^term>\<open>HOL.Ex\<close>)
- andalso (get_const_name h <> get_const_name \<^term>\<open>HOL.All\<close>)
+ andalso (dest_Const_name h <> dest_Const_name \<^term>\<open>HOL.Ex\<close>)
+ andalso (dest_Const_name h <> dest_Const_name \<^term>\<open>HOL.All\<close>)
andalso (h <> \<^term>\<open>Hilbert_Choice.Eps\<close>)
andalso (h <> \<^term>\<open>HOL.conj\<close>)
andalso (h <> \<^term>\<open>HOL.disj\<close>)
@@ -588,11 +587,10 @@
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) =>
let
val (h, args) = strip_comb t'
- val get_const_name = dest_Const #> fst
val const_h_test =
if is_Const h then
- (get_const_name h = get_const_name \<^term>\<open>HOL.Ex\<close>)
- orelse (get_const_name h = get_const_name \<^term>\<open>HOL.All\<close>)
+ (dest_Const_name h = dest_Const_name \<^term>\<open>HOL.Ex\<close>)
+ orelse (dest_Const_name h = dest_Const_name \<^term>\<open>HOL.All\<close>)
orelse (h = \<^term>\<open>Hilbert_Choice.Eps\<close>)
orelse (h = \<^term>\<open>HOL.conj\<close>)
orelse (h = \<^term>\<open>HOL.disj\<close>)
@@ -898,9 +896,7 @@
*)
val filtered_candidates =
- map (dest_Const
- #> snd
- #> use_candidate skolem_const_ty params' [])
+ map (dest_Const_type #> use_candidate skolem_const_ty params' [])
consts_candidates (* prefiltered_candidates *)
|> pair consts_candidates (* prefiltered_candidates *)
|> ListPair.zip
@@ -1076,8 +1072,7 @@
#> HOLogic.dest_eq (*the unification constraint's "="*)
#> fst
#> head_of
- #> dest_Const
- #> snd
+ #> dest_Const_type
fun arity_of ty =
let