tuned;
authorwenzelm
Sun, 16 Jul 2000 20:50:15 +0200
changeset 9356 30c3d3e308ee
parent 9355 1b2cd40579c6
child 9357 f2e806570e83
tuned;
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];