--- 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)