--- a/src/HOL/Tools/Metis/metis_generate.ML Tue Sep 21 20:56:23 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Sep 21 20:56:28 2021 +0200
@@ -71,8 +71,7 @@
fun conceal_old_skolem_terms i old_skolems t =
if exists_Const (curry (op =) \<^const_name>\<open>Meson.skolem\<close> o fst) t then
let
- fun aux old_skolems
- (t as (Const (\<^const_name>\<open>Meson.skolem\<close>, Type (_, [_, T])) $ _)) =
+ fun aux old_skolems (t as \<^Const_>\<open>Meson.skolem T for _\<close>) =
let
val (old_skolems, s) =
if i = ~1 then
@@ -114,8 +113,8 @@
if String.isPrefix lam_lifted_prefix s then
(case AList.lookup (op =) lifted s of
SOME t =>
- Const (\<^const_name>\<open>Metis.lambda\<close>, dummyT)
- $ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
+ \<^Const>\<open>Metis.lambda dummyT\<close> $
+ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
| NONE => t)
else
t
@@ -190,7 +189,7 @@
end
| metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
-fun eliminate_lam_wrappers (Const (\<^const_name>\<open>Metis.lambda\<close>, _) $ t) = eliminate_lam_wrappers t
+fun eliminate_lam_wrappers \<^Const_>\<open>Metis.lambda _ for t\<close> = eliminate_lam_wrappers t
| eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u
| eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t)
| eliminate_lam_wrappers t = t
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Sep 21 20:56:23 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Sep 21 20:56:28 2021 +0200
@@ -221,10 +221,10 @@
end
end
-fun s_not (\<^const>\<open>Not\<close> $ t) = t
+fun s_not \<^Const_>\<open>Not for t\<close> = t
| s_not t = HOLogic.mk_not t
-fun simp_not_not (\<^const>\<open>Trueprop\<close> $ t) = \<^const>\<open>Trueprop\<close> $ simp_not_not t
- | simp_not_not (\<^const>\<open>Not\<close> $ t) = s_not (simp_not_not t)
+fun simp_not_not \<^Const_>\<open>Trueprop for t\<close> = \<^Const>\<open>Trueprop for \<open>simp_not_not t\<close>\<close>
+ | simp_not_not \<^Const_>\<open>Not for t\<close> = s_not (simp_not_not t)
| simp_not_not t = t
val normalize_literal = simp_not_not o Envir.eta_contract
@@ -414,7 +414,7 @@
fun is_metis_literal_genuine (_, (s, _)) =
not (String.isPrefix class_prefix (Metis_Name.toString s))
fun is_isabelle_literal_genuine t =
- (case t of _ $ (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _) => false | _ => true)
+ (case t of _ $ \<^Const_>\<open>Meson.skolem _ for _\<close> => false | _ => true)
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
@@ -660,11 +660,11 @@
fun subst_info_of_prem subgoal_no prem =
(case prem of
- _ $ (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ (_ $ t $ num)) =>
- let val ax_no = HOLogic.dest_nat num in
- (ax_no, (subgoal_no,
- match_term (nth axioms ax_no |> the |> snd, t)))
- end
+ _ $ \<^Const_>\<open>Meson.skolem _ for \<open>_ $ t $ num\<close>\<close> =>
+ let val ax_no = HOLogic.dest_nat num in
+ (ax_no, (subgoal_no,
+ match_term (nth axioms ax_no |> the |> snd, t)))
+ end
| _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]))
fun cluster_of_var_name skolem s =
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Sep 21 20:56:23 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Sep 21 20:56:28 2021 +0200
@@ -48,12 +48,12 @@
"t => t". Type tag idempotence is also handled this way. *)
fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
(case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ t =>
+ \<^Const_>\<open>HOL.eq _ for _ t\<close> =>
let
val ct = Thm.cterm_of ctxt t
val cT = Thm.ctyp_of_cterm ct
in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
- | Const (\<^const_name>\<open>disj\<close>, _) $ t1 $ t2 =>
+ | \<^Const_>\<open>disj for t1 t2\<close> =>
(if can HOLogic.dest_not t1 then t2 else t1)
|> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
| _ => raise Fail "expected reflexive or trivial clause")
@@ -94,7 +94,7 @@
|> Thm.cterm_of ctxt
|> Conv.comb_conv (conv true ctxt))
else Conv.abs_conv (conv false o snd) ctxt ct
- | Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _ => Thm.reflexive ct
+ | \<^Const_>\<open>Meson.skolem _ for _\<close> => Thm.reflexive ct
| _ => Conv.comb_conv (conv true ctxt) ct)
val eq_th = conv true ctxt (Thm.cprop_of th)
(* We replace the equation's left-hand side with a beta-equivalent term