--- a/src/HOL/Nominal/nominal_datatype.ML Sun Aug 18 19:37:32 2024 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Aug 18 20:03:32 2024 +0200
@@ -1043,8 +1043,8 @@
val indrule_lemma = Goal.prove_global_future thy8 [] []
(Logic.mk_implies
- (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_prems),
- HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_concls)))
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj indrule_lemma_prems),
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj indrule_lemma_concls)))
(fn {context = ctxt, ...} => EVERY
[REPEAT (eresolve_tac ctxt [conjE] 1),
REPEAT (EVERY
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Sun Aug 18 19:37:32 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Sun Aug 18 20:03:32 2024 +0200
@@ -47,8 +47,6 @@
val store_thms : string -> string list -> thm list -> theory -> thm list * theory
val split_conj_thm : thm -> thm list
- val mk_conj : term list -> term
- val mk_disj : term list -> term
val app_bnds : term -> int -> term
@@ -115,9 +113,6 @@
fun split_conj_thm th =
((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
-val mk_conj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>);
-val mk_disj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.disj\<close>);
-
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
--- a/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Sun Aug 18 19:37:32 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Sun Aug 18 20:03:32 2024 +0200
@@ -44,8 +44,7 @@
in
cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
- foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
- (map HOLogic.mk_eq (frees ~~ frees')))))
+ foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (frees ~~ frees')))))
end;
in
map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
@@ -125,7 +124,7 @@
maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = Case_Translation.make_tnames recTs;
val concl =
- HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
(descr' ~~ recTs ~~ tnames)));
@@ -306,8 +305,8 @@
val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
val lhs = P $ (comb_t $ Free ("x", T));
in
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Old_Datatype_Aux.mk_conj t1s)),
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Old_Datatype_Aux.mk_disj t2s)))
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, foldr1 HOLogic.mk_conj t1s)),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ foldr1 HOLogic.mk_disj t2s)))
end
in
@@ -406,7 +405,7 @@
in
map (fn ((_, (_, _, constrs)), T) =>
HOLogic.mk_Trueprop
- (HOLogic.mk_all ("v", T, Old_Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
+ (HOLogic.mk_all ("v", T, foldr1 HOLogic.mk_disj (map (mk_eqn T) constrs))))
(hd descr ~~ newTs)
end;
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sun Aug 18 19:37:32 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sun Aug 18 20:03:32 2024 +0200
@@ -211,7 +211,7 @@
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
in
Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
- (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_ts))
(fn {context = ctxt, ...} =>
let
val induct' =