# HG changeset patch
# User paulson
# Date 1066381476 -7200
# Node ID dfae7eb2830c366d1e6b61a9dac25e6cb7d9d7a4
# Parent  d3843feb9de77c94e2d2474e21f02d7b06175dd4
Prevent recdef from looping when the inductio rule is simplified

diff -r d3843feb9de7 -r dfae7eb2830c src/HOL/Tools/recdef_package.ML
--- 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 [];