--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jun 23 18:43:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jun 24 10:38:01 2010 +0200
@@ -679,8 +679,7 @@
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
| set_mode HO =
- if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
- else HO
+ if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)