# HG changeset patch
# User wenzelm
# Date 951661607 -3600
# Node ID 93aa21ec54945cf0c5c0b23f0c28623250f251c8
# Parent  e132d147374b4f692e057d30f5a4cc53544cf512
HOLogic.dest_conj;

diff -r e132d147374b -r 93aa21ec5494 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 27 15:25:31 2000 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 27 15:26:47 2000 +0100
@@ -62,7 +62,7 @@
     val recTs = get_rec_types descr' sorts;
     val newTs = take (length (hd descr), recTs);
 
-    val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     fun prove_casedist_thm ((i, t), T) =
       let
@@ -109,7 +109,7 @@
     val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
 
-    val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     val big_rec_name' = big_name ^ "_rec_set";
     val rec_set_names = map (Sign.full_name (Theory.sign_of thy0))
diff -r e132d147374b -r 93aa21ec5494 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Sun Feb 27 15:25:31 2000 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Sun Feb 27 15:26:47 2000 +0100
@@ -46,7 +46,6 @@
   val dest_DtTFree : dtyp -> string
   val dest_DtRec : dtyp -> int
   val dest_TFree : typ -> string
-  val dest_conj : term -> term list
   val get_nonrec_types : (int * (string * dtyp list *
     (string * dtyp list) list)) list -> (string * sort) list -> typ list
   val get_branching_types : (int * (string * dtyp list *
@@ -99,15 +98,13 @@
 val mk_conj = foldr1 (HOLogic.mk_binop "op &");
 val mk_disj = foldr1 (HOLogic.mk_binop "op |");
 
-fun dest_conj (Const ("op &", _) $ t $ t') = t::(dest_conj t')
-  | dest_conj t = [t];
 
 (* instantiate induction rule *)
 
 fun indtac indrule i st =
   let
-    val ts = dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
-    val ts' = dest_conj (HOLogic.dest_Trueprop
+    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
+    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (nth_elem (i - 1, prems_of st))));
     val getP = if can HOLogic.dest_imp (hd ts) then
       (apfst Some) o HOLogic.dest_imp else pair None;
diff -r e132d147374b -r 93aa21ec5494 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Feb 27 15:25:31 2000 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Feb 27 15:26:47 2000 +0100
@@ -623,7 +623,7 @@
               [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
                etac mp 1, resolve_tac iso_elem_thms 1])]);
 
-    val Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
+    val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
     val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
       map (Free o apfst fst o dest_Var) Ps;
     val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;