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