Prevent recdef from looping when the inductio rule is simplified

--- a/src/HOL/Tools/recdef_package.ML	Fri Oct 17 11:03:48 2003 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Oct 17 11:04:36 2003 +0200
@@ -228,6 +228,7 @@
 
 fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
 
+(*"strict" is true iff (permissive) has been omitted*)
 fun gen_add_recdef tfl_fn prep_att prep_hints strict raw_name R eq_srcs hints thy =
   let
     val _ = requires_recdef thy;
@@ -240,7 +241,12 @@
     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
 
     val (cs, ss, congs, wfs) = prep_hints thy hints;
-    val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn strict thy cs ss congs wfs name R eqs;
+    (*We must remove imp_cong to prevent looping when the induction rule
+      is simplified. Many induction rules have nested implications that would
+      give rise to looping conditional rewriting.*)
+    val (thy, {rules = rules_idx, induct, tcs}) =
+        tfl_fn strict thy cs (ss delcongs [imp_cong])
+               congs wfs name R eqs;
     val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
     val simp_att = if null tcs then
       [Simplifier.simp_add_global, RecfunCodegen.add] else [];