# HG changeset patch
# User wenzelm
# Date 963773415 -7200
# Node ID 30c3d3e308eefa08ca3475641a875dd8f17d6d27
# Parent  1b2cd40579c615a78e3f12d7830dfdba1ab55a93
tuned;

diff -r 1b2cd40579c6 -r 30c3d3e308ee src/HOL/Map.ML
--- a/src/HOL/Map.ML	Sun Jul 16 20:49:56 2000 +0200
+++ b/src/HOL/Map.ML	Sun Jul 16 20:50:15 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_of Map.thy, simpset_of Map.thy));
+by (auto_tac (claset(), simpset()));
 qed "override_upd";
 Addsimps[override_upd];