src/HOL/TLA/ROOT.ML
changeset 5210 54aaa779b6b4
parent 4477 b3e5857d8d99
child 6255 db63752140c7
     1.1 --- a/src/HOL/TLA/ROOT.ML	Tue Jul 28 17:03:12 1998 +0200
     1.2 +++ b/src/HOL/TLA/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
     1.3 @@ -12,8 +12,6 @@
     1.4  *)
     1.5  Syntax.ambiguity_level := 10000;
     1.6  
     1.7 -reset global_names;
     1.8 -
     1.9  (*FIXME: the old auto_tac is sometimes needed!*)
    1.10  fun old_auto_tac (cs,ss) = 
    1.11      let val cs' = cs addss ss