# HG changeset patch
# User blanchet
# Date 1281340658 -7200
# Node ID 1954191fc6cff5262be5c2e723f6083380919778
# Parent  8672d106623c8a35b1d2fae3693a622d875629ac
fix embarrassing bug in elim rule handling, introduced during the port to FOF

diff -r 8672d106623c -r 1954191fc6cf src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 06 21:10:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 09 09:57:38 2010 +0200
@@ -212,12 +212,11 @@
    predicate variable. Leaves other theorems unchanged. We simply instantiate
    the conclusion variable to False. (Cf. "transform_elim_term" in
    "ATP_Systems".) *)
-(* FIXME: test! *)
 fun transform_elim_term t =
   case Logic.strip_imp_concl t of
     @{const Trueprop} $ Var (z, @{typ bool}) =>
-    subst_Vars [(z, @{const True})] t
-  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
+    subst_Vars [(z, @{const False})] t
+  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
   | _ => t
 
 fun presimplify_term thy =
@@ -684,7 +683,6 @@
   let
     val (ctxt, (_, th)) = goal;
     val thy = ProofContext.theory_of ctxt
-    (* ### FIXME: (1) preprocessing for "if" etc. *)
     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
     val the_axioms =
       case axioms of