1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -93,6 +93,11 @@
     1.4  (* Main function to start Metis proof and reconstruction *)
     1.5  fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
     1.6    let val thy = Proof_Context.theory_of ctxt
     1.7 +      val _ =
     1.8 +        if mode = FO then
     1.9 +          legacy_feature "Old 'metisF' command -- use 'metis' instead"
    1.10 +        else
    1.11 +          ()
    1.12        val new_skolemizer =
    1.13          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    1.14        val th_cls_pairs =