1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sat Oct 29 12:57:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Oct 29 13:15:58 2011 +0200
     1.3 @@ -208,20 +208,23 @@
     1.4             | [] =>
     1.5               case Typedef.get_info ctxt s of
     1.6                 ({abs_type, rep_type, ...}, _) :: _ =>
     1.7 -               (* We cheat here by assuming that typedef types are infinite if
     1.8 -                  their underlying type is infinite. This is unsound in general
     1.9 -                  but it's hard to think of a realistic example where this would
    1.10 -                  not be the case. We are also slack with representation types:
    1.11 -                  If a representation type has the form "sigma => tau", we
    1.12 -                  consider it enough to check "sigma" for infiniteness. (Look
    1.13 -                  for "slack" in this function.) *)
    1.14 -               (case varify_and_instantiate_type ctxt
    1.15 -                         (Logic.varifyT_global abs_type) T
    1.16 -                         (Logic.varifyT_global rep_type)
    1.17 -                     |> aux true avoid of
    1.18 -                  0 => 0
    1.19 -                | 1 => 1
    1.20 -                | _ => default_card)
    1.21 +               if not sound then
    1.22 +                 (* We cheat here by assuming that typedef types are infinite if
    1.23 +                    their underlying type is infinite. This is unsound in
    1.24 +                    general but it's hard to think of a realistic example where
    1.25 +                    this would not be the case. We are also slack with
    1.26 +                    representation types: If a representation type has the form
    1.27 +                    "sigma => tau", we consider it enough to check "sigma" for
    1.28 +                    infiniteness. *)
    1.29 +                 (case varify_and_instantiate_type ctxt
    1.30 +                           (Logic.varifyT_global abs_type) T
    1.31 +                           (Logic.varifyT_global rep_type)
    1.32 +                       |> aux true avoid of
    1.33 +                    0 => 0
    1.34 +                  | 1 => 1
    1.35 +                  | _ => default_card)
    1.36 +               else
    1.37 +                 default_card
    1.38               | [] => default_card)
    1.39            (* Very slightly unsound: Type variables are assumed not to be
    1.40               constrained to cardinality 1. (In practice, the user would most