1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 14:53:55 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 15:37:27 2010 +0200
     1.3 @@ -338,8 +338,7 @@
     1.4      |> map (snd o make_axiom ctxt)
     1.5    end
     1.6  
     1.7 -fun s_not (@{const Not} $ t) = t
     1.8 -  | s_not t = @{const Not} $ t
     1.9 +fun meta_not t = @{const "==>"} $ t $ @{prop False}
    1.10  
    1.11  fun prepare_formulas ctxt full_types hyp_ts concl_t axcls =
    1.12    let
    1.13 @@ -351,10 +350,7 @@
    1.14      val supers = tvar_classes_of_terms axtms
    1.15      val tycons = type_consts_of_terms thy (goal_t :: axtms)
    1.16      (* TFrees in the conjecture; TVars in the axioms *)
    1.17 -    val conjectures =
    1.18 -      map (s_not o HOLogic.dest_Trueprop) hyp_ts @
    1.19 -      [HOLogic.dest_Trueprop concl_t]
    1.20 -      |> make_conjectures ctxt
    1.21 +    val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
    1.22      val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls)
    1.23      val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
    1.24      val (supers', arity_clauses) = make_arity_clauses thy tycons supers