# 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*)