# HG changeset patch
# User wenzelm
# Date 1122916830 -7200
# Node ID 377962871f5d0b5f279d4320dac29da45e74e0a1
# Parent  34ed8d5d4f16ca2bf1f7f646b81d52a56341d4cd
Defs.monomorphic;

diff -r 34ed8d5d4f16 -r 377962871f5d src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Mon Aug 01 19:20:29 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Mon Aug 01 19:20:30 2005 +0200
@@ -229,12 +229,7 @@
 (*Initialize the type suppression mechanism with the current theory before
     producing any clauses!*)
 fun init thy = (curr_defs := Theory.defs_of thy);
-
-(*Types aren't needed if the constant has at most one definition and is monomorphic*)
-fun no_types_needed s =
-  (case Defs.fast_overloading_info (!curr_defs) s of
-      NONE => true
-    | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T))
+fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
     
 (*Flatten a type to a string while accumulating sort constraints on the TFress and
   TVars it contains.*)    
diff -r 34ed8d5d4f16 -r 377962871f5d src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon Aug 01 19:20:29 2005 +0200
+++ b/src/Provers/blast.ML	Mon Aug 01 19:20:30 2005 +0200
@@ -180,21 +180,15 @@
 (*Definitions of the theory in which blast is initialized.*)
 val curr_defs = ref Defs.empty;
 
-(*Types aren't needed if the constant has at most one definition and is monomorphic*)
-fun no_types_needed s =
-  (case Defs.fast_overloading_info (!curr_defs) s of
-      NONE => true
-    | 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.
   For efficiency, Const is used for FOL and for the logical constants.
   We can't use it for all non-overloaded operators because some preservation
   of type information is necessary to prevent PROOF FAILED elsewhere.*)
 fun fromConst alist (a,T) = 
-    if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse no_types_needed a 
-	then Const a 
-	else TConst(a, fromType alist T);
+  if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse
+    Defs.monomorphic (!curr_defs) a then Const a
+  else TConst(a, fromType alist T);
 
 
 (*Tests whether 2 terms are alpha-convertible; chases instantiations*)