1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -795,7 +795,8 @@
     1.4               |> fold (curry (CombApp o swap)) bound_tms
     1.5               |> type_pred_combatom type_sys res_T
     1.6               |> mk_aquant AForall (bound_names ~~ bound_Ts)
     1.7 -             |> formula_from_combformula ctxt type_sys,
     1.8 +             |> formula_from_combformula ctxt type_sys
     1.9 +             |> close_formula_universally,
    1.10               NONE, NONE)
    1.11    end
    1.12