src/HOL/Tools/recdef.ML

       give rise to looping conditional rewriting.*)
     val (thy, {rules = rules_idx, induct, tcs}) =
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
-    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add,
+    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Simps.add,
       Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy
       |> Sign.add_path bname