tuned;

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