--- a/src/HOL/TLA/ROOT.ML Tue Jul 28 17:03:12 1998 +0200
+++ b/src/HOL/TLA/ROOT.ML Tue Jul 28 17:05:34 1998 +0200
@@ -12,8 +12,6 @@
*)
Syntax.ambiguity_level := 10000;
-reset global_names;
-
(*FIXME: the old auto_tac is sometimes needed!*)
fun old_auto_tac (cs,ss) =
let val cs' = cs addss ss