src/Tools/induction.ML

--- a/src/Tools/induction.ML	Mon Dec 14 10:14:19 2015 +0100
+++ b/src/Tools/induction.ML	Mon Dec 14 11:20:31 2015 +0100
@@ -7,9 +7,12 @@
 
 signature INDUCTION =
 sig
-  val induction_tac: bool -> (binding option * (term * bool)) option list list ->
+  val induction_context_tactic: bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> context_tactic
+  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list list -> term option list -> thm list option ->
+    thm list -> int -> tactic
 end
 
 structure Induction: INDUCTION =
@@ -23,27 +26,30 @@
   | (p as Free _, _) => [p]
   | (_, ts) => maps preds_of ts);
 
-fun name_hyps (arg as ((cases, consumes), th)) =
-  if not (forall (null o #2 o #1) cases) then arg
-  else
-    let
-      val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
-      val prems' = drop consumes prems;
-      val ps = preds_of concl;
+val induction_context_tactic =
+  Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) =>
+    if not (forall (null o #2 o #1) cases) then arg
+    else
+      let
+        val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
+        val prems' = drop consumes prems;
+        val ps = preds_of concl;
+  
+        fun hname_of t =
+          if exists_subterm (member (op aconv) ps) t
+          then ind_hypsN else Rule_Cases.case_hypsN;
+  
+        val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
+        val n = Int.min (length hnamess, length cases);
+        val cases' =
+          map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
+            (take n cases ~~ take n hnamess);
+      in ((cases', consumes), th) end);
 
-      fun hname_of t =
-        if exists_subterm (member (op aconv) ps) t
-        then ind_hypsN else Rule_Cases.case_hypsN;
+fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
+  Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
 
-      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
-      val n = Int.min (length hnamess, length cases);
-      val cases' =
-        map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
-          (take n cases ~~ take n hnamess);
-    in ((cases', consumes), th) end;
-
-val induction_tac = Induct.gen_induct_tac name_hyps;
-
-val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
+val _ =
+  Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_context_tactic);
 
 end