--- 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;
--- 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);