# HG changeset patch
# User obua
# Date 1121434528 -7200
# Node ID 8ac6d4902b56c44f777f7b5357678ca116da8a61
# Parent  fade1d3a299527ad4a0ab9a97a226ffd0166ff02
optimize no_types_needed, remove exception handler

diff -r fade1d3a2995 -r 8ac6d4902b56 src/Provers/blast.ML
--- 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.