--- a/src/Provers/blast.ML Fri Jul 15 11:26:22 2005 +0200
+++ b/src/Provers/blast.ML Fri Jul 15 15:35:28 2005 +0200
@@ -182,10 +182,9 @@
(*Types aren't needed if the constant has at most one definition and is monomorphic*)
fun no_types_needed s =
- (case Defs.overloading_info (!curr_defs) s of
+ (case Defs.fast_overloading_info (!curr_defs) s of
NONE => true
- | SOME (T,defs,_) => length defs <= 1 andalso null (typ_tvars T))
- handle Option => (warning ("Defs.overloading_info failed for " ^ s); false);
+ | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T))
(*Convert a Term.Const to a Blast.Const or Blast.TConst,
converting its type to a Blast.term in the latter case.