# HG changeset patch
# User nipkow
# Date 967706581 -7200
# Node ID 252c690690b00ac48081ac12cc7caa38060ca531
# Parent  66f7eefb396717ac771c9b4d3e9ec6ba01c5483b
*** empty log message ***

diff -r 66f7eefb3967 -r 252c690690b0 TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Aug 31 01:42:23 2000 +0200
+++ b/TFL/tfl.sml	Thu Aug 31 09:23:01 2000 +0200
@@ -1045,3 +1045,6 @@
 end;
 
 end; (* TFL *)
+
+val Add_recdef_congs = Prim.Add_recdef_congs;
+val Del_recdef_congs = Prim.Del_recdef_congs;
diff -r 66f7eefb3967 -r 252c690690b0 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Aug 31 01:42:23 2000 +0200
+++ b/src/HOL/List.ML	Thu Aug 31 09:23:01 2000 +0200
@@ -326,7 +326,7 @@
 by Auto_tac;
 bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
 
-Prim.Add_recdef_congs [map_cong];
+Add_recdef_congs [map_cong];
 
 Goal "(map f xs = []) = (xs = [])";
 by (case_tac "xs" 1);