src/HOL/TLA/ROOT.ML

--- a/src/HOL/TLA/ROOT.ML	Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/ROOT.ML	Wed Dec 24 10:02:30 1997 +0100
@@ -14,6 +14,16 @@
 
 reset global_names;
 
+(*FIXME: the old auto_tac is sometimes needed!*)
+fun old_auto_tac (cs,ss) = 
+    let val cs' = cs addss ss 
+    in  EVERY [TRY (safe_tac cs'),
+               REPEAT (FIRSTGOAL (fast_tac cs')),
+               TRY (safe_tac (cs addSss ss)),
+               prune_params_tac] 
+    end;
+
+
 use_thy "TLA";
 
 val TLA_build_completed = ();