check "sound" flag before doing something unsound...

--- a/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 12:57:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -19,7 +19,7 @@
     General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
 
   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-  datatype soundness = Sound_Modulo_Infiniteness | Sound
+  datatype soundness = Sound_Modulo_Infinity | Sound
   datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
   datatype type_level =
     All_Types |
@@ -529,7 +529,7 @@
 
 datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-datatype soundness = Sound_Modulo_Infiniteness | Sound
+datatype soundness = Sound_Modulo_Infinity | Sound
 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
 datatype type_level =
   All_Types |

--- a/src/HOL/Tools/ATP/atp_util.ML	Sat Oct 29 12:57:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -208,20 +208,23 @@
            | [] =>
              case Typedef.get_info ctxt s of
                ({abs_type, rep_type, ...}, _) :: _ =>
-               (* We cheat here by assuming that typedef types are infinite if
-                  their underlying type is infinite. This is unsound in general
-                  but it's hard to think of a realistic example where this would
-                  not be the case. We are also slack with representation types:
-                  If a representation type has the form "sigma => tau", we
-                  consider it enough to check "sigma" for infiniteness. (Look
-                  for "slack" in this function.) *)
-               (case varify_and_instantiate_type ctxt
-                         (Logic.varifyT_global abs_type) T
-                         (Logic.varifyT_global rep_type)
-                     |> aux true avoid of
-                  0 => 0
-                | 1 => 1
-                | _ => default_card)
+               if not sound then
+                 (* We cheat here by assuming that typedef types are infinite if
+                    their underlying type is infinite. This is unsound in
+                    general but it's hard to think of a realistic example where
+                    this would not be the case. We are also slack with
+                    representation types: If a representation type has the form
+                    "sigma => tau", we consider it enough to check "sigma" for
+                    infiniteness. *)
+                 (case varify_and_instantiate_type ctxt
+                           (Logic.varifyT_global abs_type) T
+                           (Logic.varifyT_global rep_type)
+                       |> aux true avoid of
+                    0 => 0
+                  | 1 => 1
+                  | _ => default_card)
+               else
+                 default_card
              | [] => default_card)
           (* Very slightly unsound: Type variables are assumed not to be
              constrained to cardinality 1. (In practice, the user would most

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Oct 29 12:57:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -615,8 +615,7 @@
                 val num_facts =
                   length facts |> is_none max_relevant
                                   ? Integer.min best_max_relevant
-                val soundness =
-                  if sound then Sound else Sound_Modulo_Infiniteness
+                val soundness = if sound then Sound else Sound_Modulo_Infinity
                 val type_enc =
                   type_enc |> choose_type_enc soundness best_type_enc format
                 val fairly_sound = is_type_enc_fairly_sound type_enc