diff -r dbd98b549597 -r 5bde887b4785 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 22:06:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 23:38:09 2011 +0200
@@ -202,10 +202,10 @@
 
 fun formula_fold pos f =
   let
-    fun aux pos (AQuant (_, _, phi)) = aux pos phi
-      | aux pos (AConn conn) = aconn_fold pos aux conn
-      | aux pos (AAtom tm) = f pos tm
-  in aux pos end
+    fun fld pos (AQuant (_, _, phi)) = fld pos phi
+      | fld pos (AConn conn) = aconn_fold pos fld conn
+      | fld pos (AAtom tm) = f pos tm
+  in fld pos end
 
 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)