src/HOL/Tools/Datatype/datatype_aux.ML
changeset 32733 71618deaf777
parent 32727 9072201cd69d
child 32900 dc883c6126d4
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 21:35:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 22:47:34 2009 +0200
     1.3 @@ -35,7 +35,6 @@
     1.4  
     1.5    val app_bnds : term -> int -> term
     1.6  
     1.7 -  val cong_tac : int -> tactic
     1.8    val indtac : thm -> string list -> int -> tactic
     1.9    val exh_tac : (string -> thm) -> int -> tactic
    1.10  
    1.11 @@ -112,21 +111,6 @@
    1.12  fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
    1.13  
    1.14  
    1.15 -fun cong_tac i st = (case Logic.strip_assums_concl
    1.16 -  (List.nth (prems_of st, i - 1)) of
    1.17 -    _ $ (_ $ (f $ x) $ (g $ y)) =>
    1.18 -      let
    1.19 -        val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
    1.20 -        val _ $ (_ $ (f' $ x') $ (g' $ y')) =
    1.21 -          Logic.strip_assums_concl (prop_of cong');
    1.22 -        val insts = map (pairself (cterm_of (Thm.theory_of_thm st)) o
    1.23 -          apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
    1.24 -            apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
    1.25 -      in compose_tac (false, cterm_instantiate insts cong', 2) i st
    1.26 -        handle THM _ => no_tac st
    1.27 -      end
    1.28 -  | _ => no_tac st);
    1.29 -
    1.30  (* instantiate induction rule *)
    1.31  
    1.32  fun indtac indrule indnames i st =