src/HOL/Tools/ATP/atp_util.ML
changeset 45511 9b0f8ca4388e
parent 45299 ee584ff987c3
child 45570 6d95a66cce00
     1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Tue Nov 15 22:13:39 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Nov 15 22:13:39 2011 +0100
     1.3 @@ -268,7 +268,8 @@
     1.4  
     1.5  fun close_form t =
     1.6    fold (fn ((x, i), T) => fn t' =>
     1.7 -           HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
     1.8 +           HOLogic.all_const T
     1.9 +           $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    1.10         (Term.add_vars t []) t
    1.11  
    1.12  fun monomorphic_term subst =