1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 27 14:56:26 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 27 14:56:28 2011 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4    val typ_of_dtyp :
     1.5      Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
     1.6      -> typ
     1.7 -  val is_type_surely_finite : Proof.context -> typ -> bool
     1.8 -  val is_type_surely_infinite : Proof.context -> typ -> bool
     1.9 +  val is_type_surely_finite : Proof.context -> bool -> typ -> bool
    1.10 +  val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
    1.11    val monomorphic_term : Type.tyenv -> term -> term
    1.12    val eta_expand : typ list -> term -> int -> term
    1.13    val transform_elim_prop : term -> term
    1.14 @@ -136,7 +136,7 @@
    1.15     0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
    1.16     cardinality 2 or more. The specified default cardinality is returned if the
    1.17     cardinality of the type can't be determined. *)
    1.18 -fun tiny_card_of_type ctxt default_card T =
    1.19 +fun tiny_card_of_type ctxt sound default_card T =
    1.20    let
    1.21      val thy = Proof_Context.theory_of ctxt
    1.22      val max = 2 (* 1 would be too small for the "fun" case *)
    1.23 @@ -181,19 +181,20 @@
    1.24                         (Logic.varifyT_global abs_type) T
    1.25                         (Logic.varifyT_global rep_type)
    1.26                     |> aux true avoid of
    1.27 -                0 => 0
    1.28 +                0 => if sound then default_card else 0
    1.29                | 1 => 1
    1.30                | _ => default_card)
    1.31             | [] => default_card)
    1.32          (* Very slightly unsound: Type variables are assumed not to be
    1.33             constrained to cardinality 1. (In practice, the user would most
    1.34             likely have used "unit" directly anyway.) *)
    1.35 -      | TFree _ => if default_card = 1 then 2 else default_card
    1.36 +      | TFree _ =>
    1.37 +        if default_card = 1 andalso not sound then 2 else default_card
    1.38        | TVar _ => default_card
    1.39    in Int.min (max, aux false [] T) end
    1.40  
    1.41 -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
    1.42 -fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
    1.43 +fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
    1.44 +fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
    1.45  
    1.46  fun monomorphic_term subst =
    1.47    map_types (map_type_tvar (fn v =>