src/HOL/Tools/Sledgehammer/metis_tactics.ML

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 29 22:13:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 29 22:43:46 2010 +0200
@@ -662,7 +662,7 @@
    ("c_False", (true, @{thms True_or_False})),
    ("c_If", (true, @{thms if_True if_False True_or_False}))]
 
-fun is_quasi_fol_clause thy th =
+fun is_quasi_fol_clause thy =
   Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
 
 (* Function to generate metis clauses, including comb and type clauses *)