1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Aug 01 19:20:29 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Aug 01 19:20:30 2005 +0200
     1.3 @@ -229,12 +229,7 @@
     1.4  (*Initialize the type suppression mechanism with the current theory before
     1.5      producing any clauses!*)
     1.6  fun init thy = (curr_defs := Theory.defs_of thy);
     1.7 -
     1.8 -(*Types aren't needed if the constant has at most one definition and is monomorphic*)
     1.9 -fun no_types_needed s =
    1.10 -  (case Defs.fast_overloading_info (!curr_defs) s of
    1.11 -      NONE => true
    1.12 -    | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T))
    1.13 +fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
    1.14      
    1.15  (*Flatten a type to a string while accumulating sort constraints on the TFress and
    1.16    TVars it contains.*)    

     2.1 --- a/src/Provers/blast.ML	Mon Aug 01 19:20:29 2005 +0200
     2.2 +++ b/src/Provers/blast.ML	Mon Aug 01 19:20:30 2005 +0200
     2.3 @@ -180,21 +180,15 @@
     2.4  (*Definitions of the theory in which blast is initialized.*)
     2.5  val curr_defs = ref Defs.empty;
     2.6  
     2.7 -(*Types aren't needed if the constant has at most one definition and is monomorphic*)
     2.8 -fun no_types_needed s =
     2.9 -  (case Defs.fast_overloading_info (!curr_defs) s of
    2.10 -      NONE => true
    2.11 -    | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T))
    2.12 -
    2.13  (*Convert a Term.Const to a Blast.Const or Blast.TConst,
    2.14    converting its type to a Blast.term in the latter case.
    2.15    For efficiency, Const is used for FOL and for the logical constants.
    2.16    We can't use it for all non-overloaded operators because some preservation
    2.17    of type information is necessary to prevent PROOF FAILED elsewhere.*)
    2.18  fun fromConst alist (a,T) = 
    2.19 -    if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse no_types_needed a 
    2.20 -	then Const a 
    2.21 -	else TConst(a, fromType alist T);
    2.22 +  if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse
    2.23 +    Defs.monomorphic (!curr_defs) a then Const a
    2.24 +  else TConst(a, fromType alist T);
    2.25  
    2.26  
    2.27  (*Tests whether 2 terms are alpha-convertible; chases instantiations*)