# HG changeset patch
# User wenzelm
# Date 925202860 -7200
# Node ID e9d6f165f9c102d257cd4c75ff6b8b4e1929b2b7
# Parent  239c0eff6ce8b4ad8b82ddc2c4ee3f0c0857df48
support forward chaining;

diff -r 239c0eff6ce8 -r e9d6f165f9c1 src/HOL/Tools/induct_method.ML
--- 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");