# HG changeset patch
# User blanchet
# Date 1320738983 -3600
# Node ID 36478a5f6104f5407792d29d8bac420b02abe151
# Parent  e4e9394ddb0c97bdc9da0b441b33295c5fa71ac1
made SML/NJ happy

diff -r e4e9394ddb0c -r 36478a5f6104 src/HOL/Tools/ATP/atp_translate.ML
--- 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]