# HG changeset patch
# User wenzelm
# Date 963773448 -7200
# Node ID f2e806570e834c303a6307a6aeb8ed970a595643
# Parent  30c3d3e308eefa08ca3475641a875dd8f17d6d27
tuned;

diff -r 30c3d3e308ee -r f2e806570e83 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Sun Jul 16 20:50:15 2000 +0200
+++ b/src/HOL/Map.ML	Sun Jul 16 20:50:48 2000 +0200
@@ -147,7 +147,7 @@
 
 Goalw [override_def] "f ++ g(x|->y) = (f ++ g)(x|->y)";
 by (rtac ext 1);
-by (auto_tac (claset(), simpset()));
+by Auto_tac;
 qed "override_upd";
 Addsimps[override_upd];