--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 08 00:02:30 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 08 08:56:23 2011 +0100
@@ -787,7 +787,7 @@
#> fold (add_term_vars bounds) tms
| add_term_vars bounds (AAbs ((name, _), tm)) =
add_term_vars (name :: bounds) tm
-val close_formula_universally = close_universally add_term_vars
+fun close_formula_universally phi = close_universally add_term_vars phi
fun add_iterm_vars bounds (IApp (tm1, tm2)) =
fold (add_iterm_vars bounds) [tm1, tm2]