src/HOL/Tools/datatype_aux.ML
changeset 8305 93aa21ec5494
parent 7015 85be09eb136c
child 8324 df7dccddc3de
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Sun Feb 27 15:25:31 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sun Feb 27 15:26:47 2000 +0100
     1.3 @@ -46,7 +46,6 @@
     1.4    val dest_DtTFree : dtyp -> string
     1.5    val dest_DtRec : dtyp -> int
     1.6    val dest_TFree : typ -> string
     1.7 -  val dest_conj : term -> term list
     1.8    val get_nonrec_types : (int * (string * dtyp list *
     1.9      (string * dtyp list) list)) list -> (string * sort) list -> typ list
    1.10    val get_branching_types : (int * (string * dtyp list *
    1.11 @@ -99,15 +98,13 @@
    1.12  val mk_conj = foldr1 (HOLogic.mk_binop "op &");
    1.13  val mk_disj = foldr1 (HOLogic.mk_binop "op |");
    1.14  
    1.15 -fun dest_conj (Const ("op &", _) $ t $ t') = t::(dest_conj t')
    1.16 -  | dest_conj t = [t];
    1.17  
    1.18  (* instantiate induction rule *)
    1.19  
    1.20  fun indtac indrule i st =
    1.21    let
    1.22 -    val ts = dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
    1.23 -    val ts' = dest_conj (HOLogic.dest_Trueprop
    1.24 +    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
    1.25 +    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
    1.26        (Logic.strip_imp_concl (nth_elem (i - 1, prems_of st))));
    1.27      val getP = if can HOLogic.dest_imp (hd ts) then
    1.28        (apfst Some) o HOLogic.dest_imp else pair None;