# HG changeset patch
# User blanchet
# Date 1280410647 -7200
# Node ID c802b76d542f54a65aae6695c6d20f2a0c9a9d25
# Parent  cc44e887246c481b807eb8149af7fe322ab03852
don't assume canonical rule format

diff -r cc44e887246c -r c802b76d542f src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 14:53:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 15:37:27 2010 +0200
@@ -338,8 +338,7 @@
     |> map (snd o make_axiom ctxt)
   end
 
-fun s_not (@{const Not} $ t) = t
-  | s_not t = @{const Not} $ t
+fun meta_not t = @{const "==>"} $ t $ @{prop False}
 
 fun prepare_formulas ctxt full_types hyp_ts concl_t axcls =
   let
@@ -351,10 +350,7 @@
     val supers = tvar_classes_of_terms axtms
     val tycons = type_consts_of_terms thy (goal_t :: axtms)
     (* TFrees in the conjecture; TVars in the axioms *)
-    val conjectures =
-      map (s_not o HOLogic.dest_Trueprop) hyp_ts @
-      [HOLogic.dest_Trueprop concl_t]
-      |> make_conjectures ctxt
+    val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
     val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls)
     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers