src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 37538 97ab019d5ac8
parent 37516 c81c86bfc18a
child 37548 6a7a9261b9ad
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 23 18:43:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jun 24 10:38:01 2010 +0200
     1.3 @@ -679,8 +679,7 @@
     1.4        (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
     1.5        fun set_mode FO = FO
     1.6          | set_mode HO =
     1.7 -          if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
     1.8 -          else HO
     1.9 +          if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO
    1.10          | set_mode FT = FT
    1.11        val mode = set_mode mode0
    1.12        (*transform isabelle clause to metis clause *)