# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID 7a0b858fa63b42607637da85ad602481f07ed651
# Parent  ec5e62b868ebfcc3b5a91fa66ef5d06de6673380
don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway

diff -r ec5e62b868eb -r 7a0b858fa63b src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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)) =>