src/HOL/List.ML

 by (hyp_subst_tac 1);
 by (induct_tac "ys" 1);
 by Auto_tac;
 bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
 
-Add_recdef_congs [map_cong];
-
 Goal "(map f xs = []) = (xs = [])";
 by (case_tac "xs" 1);
 by Auto_tac;
 qed "map_is_Nil_conv";
 AddIffs [map_is_Nil_conv];