--- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 28 21:35:57 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 28 22:47:34 2009 +0200
@@ -35,7 +35,6 @@
val app_bnds : term -> int -> term
- val cong_tac : int -> tactic
val indtac : thm -> string list -> int -> tactic
val exh_tac : (string -> thm) -> int -> tactic
@@ -112,21 +111,6 @@
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
-fun cong_tac i st = (case Logic.strip_assums_concl
- (List.nth (prems_of st, i - 1)) of
- _ $ (_ $ (f $ x) $ (g $ y)) =>
- let
- val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
- val _ $ (_ $ (f' $ x') $ (g' $ y')) =
- Logic.strip_assums_concl (prop_of cong');
- val insts = map (pairself (cterm_of (Thm.theory_of_thm st)) o
- apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
- apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
- in compose_tac (false, cterm_instantiate insts cong', 2) i st
- handle THM _ => no_tac st
- end
- | _ => no_tac st);
-
(* instantiate induction rule *)
fun indtac indrule indnames i st =