# HG changeset patch
# User wenzelm
# Date 1133301620 -3600
# Node ID 28efcdae34dc971f4280fd7d9fc993c827201ed9
# Parent  7273cf5085ed5ab75cca90bf918a2e205721332a
moved nth_list to Pure/library.ML;

diff -r 7273cf5085ed -r 28efcdae34dc src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Tue Nov 29 23:00:03 2005 +0100
+++ b/src/Provers/induct_method.ML	Tue Nov 29 23:00:20 2005 +0100
@@ -20,6 +20,8 @@
 signature INDUCT_METHOD =
 sig
   val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
+  val add_defs: (string option * term) option list -> Proof.context ->
+    (term option list * thm list) * Proof.context
   val atomize_term: theory -> term -> term
   val atomize_tac: int -> tactic
   val rulified_term: thm -> theory * term
@@ -40,9 +42,7 @@
 
 (** misc utils **)
 
-(* lists *)
-
-fun nth_list xss i = nth xss i handle Subscript => [];
+(* alignment *)
 
 fun align_left msg xs ys =
   let val m = length xs and n = length ys