--- 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)}]
--- a/src/HOL/Library/Pattern_Aliases.thy Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy Tue Sep 28 22:14:44 2021 +0200
@@ -97,7 +97,7 @@
fun check_pattern_syntax t =
case strip_all t of
- (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+ (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
let
fun go (Const (\<^const_name>\<open>as\<close>, _) $ pat $ var, rhs) =
let
@@ -126,7 +126,7 @@
fun uncheck_pattern_syntax ctxt t =
case strip_all t of
- (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+ (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
let
(* restricted to going down abstractions; ignores eta-contracted rhs *)
fun go lhs (rhs as Const (\<^const_name>\<open>Let\<close>, _) $ pat $ Abs (name, typ, t)) ctxt frees =
--- a/src/HOL/Library/code_lazy.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Tue Sep 28 22:14:44 2021 +0200
@@ -378,8 +378,8 @@
||>> fold_map (mk_name ("case_" ^ short_type_name ^ "_lazy_") "") ctr_names
val mk_Lazy_delay_eq =
- (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^const>\<open>Unity\<close>))
- |> mk_eq |> all_abs [\<^typ>\<open>unit\<close> --> lazy_type]
+ (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^Const>\<open>Unity\<close>))
+ |> mk_eq |> all_abs [\<^Type>\<open>unit\<close> --> lazy_type]
val (Lazy_delay_thm, lthy8a) = mk_thm
((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}])
lthy8
--- a/src/HOL/Library/code_test.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/code_test.ML Tue Sep 28 22:14:44 2021 +0200
@@ -179,15 +179,15 @@
lhs :: rhs :: acc)
| add_eval _ = I
-fun mk_term_of [] = \<^term>\<open>None :: (unit \<Rightarrow> yxml_of_term) option\<close>
+fun mk_term_of [] = \<^Const>\<open>None \<^typ>\<open>unit \<Rightarrow> yxml_of_term\<close>\<close>
| mk_term_of ts =
let
val tuple = mk_tuples ts
val T = fastype_of tuple
in
\<^term>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $
- (absdummy \<^typ>\<open>unit\<close> (\<^const>\<open>yxml_string_of_term\<close> $
- (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^typ>\<open>term\<close>) $ tuple)))
+ (absdummy \<^typ>\<open>unit\<close> (\<^Const>\<open>yxml_string_of_term\<close> $
+ (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^Type>\<open>term\<close>) $ tuple)))
end
fun test_terms ctxt ts target =
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Sep 28 22:14:44 2021 +0200
@@ -303,11 +303,11 @@
fun name_of_disc t =
(case head_of t of
- Abs (_, _, \<^const>\<open>Not\<close> $ (t' $ Bound 0)) =>
+ Abs (_, _, \<^Const_>\<open>Not for \<open>t' $ Bound 0\<close>\<close>) =>
Long_Name.map_base_name (prefix not_prefix) (name_of_disc t')
- | Abs (_, _, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Bound 0 $ t') =>
+ | Abs (_, _, \<^Const_>\<open>HOL.eq _ for \<open>Bound 0\<close> t'\<close>) =>
Long_Name.map_base_name (prefix is_prefix) (name_of_disc t')
- | Abs (_, _, \<^const>\<open>Not\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Bound 0 $ t')) =>
+ | Abs (_, _, \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for \<open>Bound 0\<close> t'\<close>\<close>) =>
Long_Name.map_base_name (prefix (not_prefix ^ is_prefix)) (name_of_disc t')
| t' => name_of_const "discriminator" (perhaps (try domain_type)) t');
@@ -1037,7 +1037,7 @@
val disc_eq_case_thms =
let
- fun const_of_bool b = if b then \<^const>\<open>True\<close> else \<^const>\<open>False\<close>;
+ fun const_of_bool b = if b then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>;
fun mk_case_args n = map_index (fn (k, argTs) =>
fold_rev Term.absdummy argTs (const_of_bool (n = k))) ctr_Tss;
val goals = map_index (fn (n, udisc) =>
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Sep 28 22:14:44 2021 +0200
@@ -400,7 +400,7 @@
let val (sel_rhs, wits) = mk_sel_case_args lthy4 ctr_Tss ks arg
in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end;
fun mk_dis_case_args args k = map (fn (k', arg) => (if k = k'
- then fold_rev Term.lambda arg \<^const>\<open>True\<close> else fold_rev Term.lambda arg \<^const>\<open>False\<close>)) args;
+ then fold_rev Term.lambda arg \<^Const>\<open>True\<close> else fold_rev Term.lambda arg \<^Const>\<open>False\<close>)) args;
val sel_rhs = map (map mk_sel_rhs) sel_argss
val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks
val dis_qty = qty_isom --> HOLogic.boolT;
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML Tue Sep 28 22:14:44 2021 +0200
@@ -131,7 +131,7 @@
fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns;
-fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close> $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true
+fun has_lonely_bool_var \<^Const_>\<open>Pure.conjunction for \<^Const_>\<open>Trueprop for \<open>Free _\<close>\<close> _\<close> = true
| has_lonely_bool_var _ = false;
val syntactic_sorts =
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Sep 28 22:14:44 2021 +0200
@@ -240,7 +240,7 @@
fun mutual_co_datatypes_of ctxt (T_name, Ts) =
(if T_name = \<^type_name>\<open>itself\<close> then
- (BNF_Util.Least_FP, [\<^typ>\<open>'a itself\<close>], [[@{const Pure.type ('a)}]])
+ (BNF_Util.Least_FP, [\<^typ>\<open>'a itself\<close>], [[\<^Const>\<open>Pure.type \<^typ>\<open>'a\<close>\<close>]])
else
let
val (fp, ctr_sugars) =
@@ -269,7 +269,7 @@
val A = Logic.varifyT_global \<^typ>\<open>'a\<close>;
val absT = Type (\<^type_name>\<open>set\<close>, [A]);
val repT = A --> HOLogic.boolT;
- val pred = Abs (Name.uu, repT, \<^const>\<open>True\<close>);
+ val pred = Abs (Name.uu, repT, \<^Const>\<open>True\<close>);
val abs = Const (\<^const_name>\<open>Collect\<close>, repT --> absT);
val rep = Const (\<^const_name>\<open>rmember\<close>, absT --> repT);
in
@@ -518,8 +518,8 @@
fold process_spec specs NONE
end;
-fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t
- | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
+fun lhs_of_equation \<^Const_>\<open>Pure.eq _ for t _\<close> = t
+ | lhs_of_equation \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t _\<close>\<close> = t;
fun specialize_definition_type thy x def0 =
let
@@ -674,10 +674,10 @@
[cmd] :: (group :: groups)
end;
-fun defined_by (Const (\<^const_name>\<open>All\<close>, _) $ t) = defined_by t
+fun defined_by \<^Const_>\<open>All _ for t\<close> = defined_by t
| defined_by (Abs (_, _, t)) = defined_by t
- | defined_by (\<^const>\<open>implies\<close> $ _ $ u) = defined_by u
- | defined_by (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) = head_of t
+ | defined_by \<^Const_>\<open>implies for _ u\<close> = defined_by u
+ | defined_by \<^Const_>\<open>HOL.eq _ for t _\<close> = head_of t
| defined_by t = head_of t;
fun partition_props [_] props = SOME [props]
@@ -1002,14 +1002,14 @@
val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt
|> List.partition has_polymorphism;
- fun implicit_evals_of pol (\<^const>\<open>Not\<close> $ t) = implicit_evals_of (not pol) t
- | implicit_evals_of pol (\<^const>\<open>implies\<close> $ t $ u) =
+ fun implicit_evals_of pol \<^Const_>\<open>Not for t\<close> = implicit_evals_of (not pol) t
+ | implicit_evals_of pol \<^Const_>\<open>implies for t u\<close> =
(case implicit_evals_of pol u of
[] => implicit_evals_of (not pol) t
| ts => ts)
- | implicit_evals_of pol (\<^const>\<open>conj\<close> $ t $ u) =
+ | implicit_evals_of pol \<^Const_>\<open>conj for t u\<close> =
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
- | implicit_evals_of pol (\<^const>\<open>disj\<close> $ t $ u) =
+ | implicit_evals_of pol \<^Const_>\<open>disj for t u\<close> =
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
| implicit_evals_of false (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) =
distinct (op aconv) [t, u]
@@ -1049,7 +1049,7 @@
Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t);
fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body
- | is_triv_wrt \<^const>\<open>True\<close> = true
+ | is_triv_wrt \<^Const>\<open>True\<close> = true
| is_triv_wrt _ = false;
fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} =
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Tue Sep 28 22:14:44 2021 +0200
@@ -166,11 +166,11 @@
else if id = nun_equals then
Const (\<^const_name>\<open>HOL.eq\<close>, typ_of ty)
else if id = nun_false then
- \<^const>\<open>False\<close>
+ \<^Const>\<open>False\<close>
else if id = nun_if then
Const (\<^const_name>\<open>If\<close>, typ_of ty)
else if id = nun_implies then
- \<^term>\<open>implies\<close>
+ \<^Const>\<open>implies\<close>
else if id = nun_not then
HOLogic.Not
else if id = nun_unique then
@@ -178,7 +178,7 @@
else if id = nun_unique_unsafe then
Const (\<^const_name>\<open>The_unsafe\<close>, typ_of ty)
else if id = nun_true then
- \<^const>\<open>True\<close>
+ \<^Const>\<open>True\<close>
else if String.isPrefix nun_dollar_anon_fun_prefix id then
let val j = Int.fromString (unprefix nun_dollar_anon_fun_prefix id) |> the_default ~1 in
Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty)
@@ -225,12 +225,12 @@
end
| term_of _ (NMatch _) = raise Fail "unexpected match";
- fun rewrite_numbers (t as \<^const>\<open>Suc\<close> $ _) =
+ fun rewrite_numbers (t as \<^Const>\<open>Suc\<close> $ _) =
(case try HOLogic.dest_nat t of
- SOME n => HOLogic.mk_number \<^typ>\<open>nat\<close> n
+ SOME n => HOLogic.mk_number \<^Type>\<open>nat\<close> n
| NONE => t)
- | rewrite_numbers (\<^const>\<open>Abs_Integ\<close> $ (@{const Pair (nat, nat)} $ t $ u)) =
- HOLogic.mk_number \<^typ>\<open>int\<close> (HOLogic.dest_nat t - HOLogic.dest_nat u)
+ | rewrite_numbers \<^Const_>\<open>Abs_Integ for \<^Const>\<open>Pair \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t u\<close>\<close> =
+ HOLogic.mk_number \<^Type>\<open>int\<close> (HOLogic.dest_nat t - HOLogic.dest_nat u)
| rewrite_numbers (t $ u) = rewrite_numbers t $ rewrite_numbers u
| rewrite_numbers (Abs (s, T, t)) = Abs (s, T, rewrite_numbers t)
| rewrite_numbers t = t;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Sep 28 22:14:44 2021 +0200
@@ -466,8 +466,8 @@
fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
fun make_set T1 [] = Const (\<^const_abbrev>\<open>Set.empty\<close>, T1 --> \<^typ>\<open>bool\<close>)
- | make_set T1 ((_, \<^const>\<open>False\<close>) :: tps) = make_set T1 tps
- | make_set T1 ((t1, \<^const>\<open>True\<close>) :: tps) =
+ | make_set T1 ((_, \<^Const_>\<open>False\<close>) :: tps) = make_set T1 tps
+ | make_set T1 ((t1, \<^Const_>\<open>True\<close>) :: tps) =
Const (\<^const_name>\<open>insert\<close>, T1 --> (T1 --> \<^typ>\<open>bool\<close>) --> T1 --> \<^typ>\<open>bool\<close>) $
t1 $ (make_set T1 tps)
| make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
@@ -476,8 +476,8 @@
| make_coset T tps =
let
val U = T --> \<^typ>\<open>bool\<close>
- fun invert \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
- | invert \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
+ fun invert \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+ | invert \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
in
Const (\<^const_name>\<open>Groups.minus_class.minus\<close>, U --> U --> U) $
Const (\<^const_abbrev>\<open>UNIV\<close>, U) $ make_set T (map (apsnd invert) tps)
@@ -505,8 +505,8 @@
(case T2 of
\<^typ>\<open>bool\<close> =>
(case t of
- Abs(_, _, \<^const>\<open>False\<close>) => fst #> rev #> make_set T1
- | Abs(_, _, \<^const>\<open>True\<close>) => fst #> rev #> make_coset T1
+ Abs(_, _, \<^Const_>\<open>False\<close>) => fst #> rev #> make_set T1
+ | Abs(_, _, \<^Const_>\<open>True\<close>) => fst #> rev #> make_coset T1
| Abs(_, _, Const (\<^const_name>\<open>undefined\<close>, _)) => fst #> rev #> make_set T1
| _ => raise TERM ("post_process_term", [t]))
| Type (\<^type_name>\<open>option\<close>, _) =>
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Tue Sep 28 22:14:44 2021 +0200
@@ -96,7 +96,7 @@
fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
val t_rhs = lambda t_k proto_t_rhs;
val eqs0 = [subst_v \<^term>\<open>0::natural\<close> eq,
- subst_v (\<^const>\<open>Code_Numeral.Suc\<close> $ t_k) eq];
+ subst_v \<^Const>\<open>Code_Numeral.Suc for t_k\<close> eq];
val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
val ((_, (_, eqs2)), lthy') = lthy
|> BNF_LFP_Compat.primrec_simple
--- a/src/HOL/Tools/Transfer/transfer.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Tue Sep 28 22:14:44 2021 +0200
@@ -550,8 +550,8 @@
Symtab.join (K or3) (tab1, tab2)
end
val tab = go [] p (t, u) Symtab.empty
- fun f (a, (true, false, false)) = SOME (a, \<^const>\<open>implies\<close>)
- | f (a, (false, true, false)) = SOME (a, \<^const>\<open>rev_implies\<close>)
+ fun f (a, (true, false, false)) = SOME (a, \<^Const>\<open>implies\<close>)
+ | f (a, (false, true, false)) = SOME (a, \<^Const>\<open>rev_implies\<close>)
| f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT)
| f _ = NONE
in
--- a/src/HOL/Tools/record.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/record.ML Tue Sep 28 22:14:44 2021 +0200
@@ -1808,8 +1808,8 @@
distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
split_sels = [], split_sel_asms = [], case_eq_ifs = []};
-fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t
- | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
+fun lhs_of_equation \<^Const_>\<open>Pure.eq _ for t _\<close> = t
+ | lhs_of_equation \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t _\<close>\<close> = t;
fun add_spec_rule rule =
let val head = head_of (lhs_of_equation (Thm.prop_of rule))
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Tue Sep 28 22:14:44 2021 +0200
@@ -250,8 +250,8 @@
(map Pattern pats, Un (fm1', fm2'))
end;
-fun mk_formula vs (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) = merge_inter vs (mk_formula vs t1) (mk_formula vs t2)
- | mk_formula vs (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) = merge_union vs (mk_formula vs t1) (mk_formula vs t2)
+fun mk_formula vs \<^Const_>\<open>conj for t1 t2\<close> = merge_inter vs (mk_formula vs t1) (mk_formula vs t2)
+ | mk_formula vs \<^Const_>\<open>disj for t1 t2\<close> = merge_union vs (mk_formula vs t1) (mk_formula vs t2)
| mk_formula vs t = apfst single (mk_atom vs t)
fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2)