# HG changeset patch
# User wenzelm
# Date 968172447 -7200
# Node ID 5c6425d83501f264067a8236695e05cebaf01012
# Parent  6ca7fcac3e232ba5e237ba01f484b0185de2e4f1
removed Add_recdef_congs [map_cong] (see Main.thy);

diff -r 6ca7fcac3e23 -r 5c6425d83501 src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Sep 05 18:47:03 2000 +0200
+++ b/src/HOL/List.ML	Tue Sep 05 18:47:27 2000 +0200
@@ -326,8 +326,6 @@
 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;