1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -267,9 +267,9 @@
     1.4    | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
     1.5  
     1.6  fun close_form t =
     1.7 -  fold (fn ((x, i), T) => fn t' =>
     1.8 +  fold (fn ((s, i), T) => fn t' =>
     1.9             HOLogic.all_const T
    1.10 -           $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    1.11 +           $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
    1.12         (Term.add_vars t []) t
    1.13  
    1.14  fun monomorphic_term subst =