# HG changeset patch
# User berghofe
# Date 1218589233 -7200
# Node ID 0dffedf9aff5a91b0f994ce5e0daf1af0104781b
# Parent  2828a276dc9330ea96495a35c8cc668904dcca79
Changed proof of strong induction rule to avoid infinite loop
when premises of introduction rules contain equations.

diff -r 2828a276dc93 -r 0dffedf9aff5 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Aug 12 21:48:59 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 13 03:00:33 2008 +0200
@@ -388,9 +388,10 @@
                      REPEAT_DETERM_N (nprems_of ihyp - length gprems)
                        (simp_tac swap_simps_ss 1),
                      REPEAT_DETERM_N (length gprems)
-                       (simp_tac (HOL_ss
-                          addsimps inductive_forall_def' :: gprems2
-                          addsimprocs [NominalPackage.perm_simproc]) 1)]));
+                       (simp_tac (HOL_basic_ss
+                          addsimps [inductive_forall_def']
+                          addsimprocs [NominalPackage.perm_simproc]) 1 THEN
+                        resolve_tac gprems2 1)]));
                  val final = Goal.prove ctxt'' [] [] (term_of concl)
                    (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
                      addsimps vc_compat_ths'' @ freshs2' @