src/HOL/Tools/datatype_aux.ML
changeset 8305 93aa21ec5494
parent 7015 85be09eb136c
child 8324 df7dccddc3de
--- 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;