src/HOL/Tools/recdef_package.ML
changeset 14241 dfae7eb2830c
parent 12876 a70df1e5bf10
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Oct 17 11:03:48 2003 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Oct 17 11:04:36 2003 +0200
     1.3 @@ -228,6 +228,7 @@
     1.4  
     1.5  fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
     1.6  
     1.7 +(*"strict" is true iff (permissive) has been omitted*)
     1.8  fun gen_add_recdef tfl_fn prep_att prep_hints strict raw_name R eq_srcs hints thy =
     1.9    let
    1.10      val _ = requires_recdef thy;
    1.11 @@ -240,7 +241,12 @@
    1.12      val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    1.13  
    1.14      val (cs, ss, congs, wfs) = prep_hints thy hints;
    1.15 -    val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn strict thy cs ss congs wfs name R eqs;
    1.16 +    (*We must remove imp_cong to prevent looping when the induction rule
    1.17 +      is simplified. Many induction rules have nested implications that would
    1.18 +      give rise to looping conditional rewriting.*)
    1.19 +    val (thy, {rules = rules_idx, induct, tcs}) =
    1.20 +        tfl_fn strict thy cs (ss delcongs [imp_cong])
    1.21 +               congs wfs name R eqs;
    1.22      val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
    1.23      val simp_att = if null tcs then
    1.24        [Simplifier.simp_add_global, RecfunCodegen.add] else [];