1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 12:57:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4      General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
     1.5  
     1.6    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
     1.7 -  datatype soundness = Sound_Modulo_Infiniteness | Sound
     1.8 +  datatype soundness = Sound_Modulo_Infinity | Sound
     1.9    datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
    1.10    datatype type_level =
    1.11      All_Types |
    1.12 @@ -529,7 +529,7 @@
    1.13  
    1.14  datatype order = First_Order | Higher_Order
    1.15  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    1.16 -datatype soundness = Sound_Modulo_Infiniteness | Sound
    1.17 +datatype soundness = Sound_Modulo_Infinity | Sound
    1.18  datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
    1.19  datatype type_level =
    1.20    All_Types |

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sat Oct 29 12:57:43 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Oct 29 13:15:58 2011 +0200
     2.3 @@ -208,20 +208,23 @@
     2.4             | [] =>
     2.5               case Typedef.get_info ctxt s of
     2.6                 ({abs_type, rep_type, ...}, _) :: _ =>
     2.7 -               (* We cheat here by assuming that typedef types are infinite if
     2.8 -                  their underlying type is infinite. This is unsound in general
     2.9 -                  but it's hard to think of a realistic example where this would
    2.10 -                  not be the case. We are also slack with representation types:
    2.11 -                  If a representation type has the form "sigma => tau", we
    2.12 -                  consider it enough to check "sigma" for infiniteness. (Look
    2.13 -                  for "slack" in this function.) *)
    2.14 -               (case varify_and_instantiate_type ctxt
    2.15 -                         (Logic.varifyT_global abs_type) T
    2.16 -                         (Logic.varifyT_global rep_type)
    2.17 -                     |> aux true avoid of
    2.18 -                  0 => 0
    2.19 -                | 1 => 1
    2.20 -                | _ => default_card)
    2.21 +               if not sound then
    2.22 +                 (* We cheat here by assuming that typedef types are infinite if
    2.23 +                    their underlying type is infinite. This is unsound in
    2.24 +                    general but it's hard to think of a realistic example where
    2.25 +                    this would not be the case. We are also slack with
    2.26 +                    representation types: If a representation type has the form
    2.27 +                    "sigma => tau", we consider it enough to check "sigma" for
    2.28 +                    infiniteness. *)
    2.29 +                 (case varify_and_instantiate_type ctxt
    2.30 +                           (Logic.varifyT_global abs_type) T
    2.31 +                           (Logic.varifyT_global rep_type)
    2.32 +                       |> aux true avoid of
    2.33 +                    0 => 0
    2.34 +                  | 1 => 1
    2.35 +                  | _ => default_card)
    2.36 +               else
    2.37 +                 default_card
    2.38               | [] => default_card)
    2.39            (* Very slightly unsound: Type variables are assumed not to be
    2.40               constrained to cardinality 1. (In practice, the user would most

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