# HG changeset patch
# User paulson
# Date 869651426 -7200
# Node ID c4f13747489f5dd00b9270f8857df499dbd44f56
# Parent  5380acac8c8331b5e29c65cdd9da45dcc73f8788
Uses new version of Datatype.occs_in_prems

diff -r 5380acac8c83 -r c4f13747489f src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Jul 23 11:49:20 1997 +0200
+++ b/src/HOL/NatDef.ML	Wed Jul 23 11:50:26 1997 +0200
@@ -41,10 +41,11 @@
 qed "nat_induct";
 
 (*Perform induction on n. *)
-fun nat_ind_tac a i = 
-    EVERY[res_inst_tac [("n",a)] nat_induct i,
-          COND (Datatype.occs_in_prems a (i+1)) all_tac
-               (rename_last_tac a [""] (i+1))];
+local fun raw_nat_ind_tac a i = 
+    res_inst_tac [("n",a)] nat_induct i  THEN  rename_last_tac a [""] (i+1)
+in
+val nat_ind_tac = Datatype.occs_in_prems raw_nat_ind_tac
+end;
 
 (*A special form of induction for reasoning about m<n and m-n*)
 val prems = goal thy