# HG changeset patch
# User wenzelm
# Date 1724004212 -7200
# Node ID dff10bb4ebdb557a7809ab4c9fdef5ecec22fd9f
# Parent  bb292fc53f82b1b1cced9b9602b54c4a0158bfa3
clarified signature: eliminate clones;

diff -r bb292fc53f82 -r dff10bb4ebdb src/HOL/Nominal/nominal_datatype.ML
--- 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
diff -r bb292fc53f82 -r dff10bb4ebdb src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- 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));
 
 
diff -r bb292fc53f82 -r dff10bb4ebdb src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
--- 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;
 
diff -r bb292fc53f82 -r dff10bb4ebdb src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- 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' =