1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 06 10:35:05 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 06 10:35:05 2012 +0200
     1.3 @@ -679,7 +679,7 @@
     1.4                  val soundness = if strict then Strict else Non_Strict
     1.5                  val type_enc =
     1.6                    type_enc |> choose_type_enc soundness best_type_enc format
     1.7 -                val fairly_sound = is_type_enc_fairly_sound type_enc
     1.8 +                val sound = is_type_enc_sound type_enc
     1.9                  val real_ms = Real.fromInt o Time.toMilliseconds
    1.10                  val slice_timeout =
    1.11                    ((real_ms time_left
    1.12 @@ -714,7 +714,7 @@
    1.13                    else
    1.14                      facts
    1.15                      |> map untranslated_fact
    1.16 -                    |> not fairly_sound
    1.17 +                    |> not sound
    1.18                         ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
    1.19                      |> take num_facts
    1.20                      |> polymorphism_of_type_enc type_enc <> Polymorphic
    1.21 @@ -764,11 +764,8 @@
    1.22                         SOME facts =>
    1.23                         let
    1.24                           val failure =
    1.25 -                           if null facts then
    1.26 -                             ProofIncomplete
    1.27 -                           else
    1.28 -                             UnsoundProof (is_type_enc_quasi_sound type_enc,
    1.29 -                                           facts)
    1.30 +                           if null facts then ProofIncomplete
    1.31 +                           else UnsoundProof (is_type_enc_sound type_enc, facts)
    1.32                         in
    1.33                           if debug then
    1.34                             (warning (string_for_failure failure); NONE)