src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -267,7 +267,7 @@
   in  Goal.prove_internal [ex_tm] conc tacf
        |> forall_intr_list frees
        |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
-       |> Thm.varifyT
+       |> Thm.varifyT_global
   end;