--- a/src/HOL/Tools/induct_method.ML Tue Apr 27 10:46:37 1999 +0200
+++ b/src/HOL/Tools/induct_method.ML Tue Apr 27 10:47:40 1999 +0200
@@ -40,7 +40,7 @@
(* induct_tac *)
-fun induct_tac thy insts opt_kind_name i state =
+fun induct_tac thy insts opt_kind_name facts i state =
let
val (kind, name) =
(case opt_kind_name of Some kind_name => kind_name | None =>
@@ -62,7 +62,7 @@
if null insts then rule
else Drule.cterm_instantiate (prep_insts
(DatatypeAux.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule)), insts)) rule;
- in Tactic.rtac inst_rule i state end;
+ in Method.rule_tac [inst_rule] facts i state end;
(* induct_method *)
@@ -72,7 +72,7 @@
fun induct ctxt =
Args.and_list inst -- Scan.option (Scan.lift (kind -- Args.name))
- >> (fn (is, k) => Method.METHOD0 (FIRSTGOAL (induct_tac (ProofContext.theory_of ctxt) is k)));
+ >> (fn (is, k) => Method.METHOD (FIRSTGOAL o induct_tac (ProofContext.theory_of ctxt) is k));
fun induct_meth src ctxt = #2 (Method.syntax (induct ctxt) ctxt src);
val induct_method = ("induct", induct_meth, "induction on types / sets / functions");