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