--- 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))
--- 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;
--- 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;