# HG changeset patch
# User blanchet
# Date 1316077060 -7200
# Node ID 2302faa4ae0e1ebb6f148d0a66718e235511d626
# Parent  9795fdc87965c45782c8b6c95ff37a248365a2e4
tuning

diff -r 9795fdc87965 -r 2302faa4ae0e src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Sep 15 09:44:27 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Sep 15 10:57:40 2011 +0200
@@ -22,6 +22,7 @@
   val trace : bool Config.T
   val verbose : bool Config.T
   val new_skolemizer : bool Config.T
+  val type_has_top_sort : typ -> bool
   val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
   val setup : theory -> theory
 end
diff -r 9795fdc87965 -r 2302faa4ae0e src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Sep 15 09:44:27 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Sep 15 10:57:40 2011 +0200
@@ -63,6 +63,7 @@
 struct
 
 open ATP_Translate
+open Metis_Tactic
 open Sledgehammer_Util
 
 val trace =
@@ -786,9 +787,6 @@
   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
                            | _ => false) (prop_of th)
 
-val type_has_top_sort =
-  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
 (**** Predicates to detect unwanted facts (prolific or likely to cause
       unsoundness) ****)