don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 05 10:12:54 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jun 06 10:35:05 2012 +0200
@@ -1302,11 +1302,8 @@
   end
 
 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
-  | s_not_prop _ = @{prop True} (* "t" is too meta for "metis" *)
-(*
   | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
   | s_not_prop t = @{const "==>"} $ t $ @{prop False}
-*)
 
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (role, t)) =>