1.1 --- a/NEWS	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/NEWS	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -85,6 +85,9 @@
     1.4      TPTP problems (TFF).
     1.5    - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
     1.6  
     1.7 +* Metis:
     1.8 +  - Obsoleted "metisF" -- use "metis" instead.
     1.9 +
    1.10  * "try":
    1.11    - Added "simp:", "intro:", and "elim:" options.
    1.12  

     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     2.3 @@ -93,6 +93,11 @@
     2.4  (* Main function to start Metis proof and reconstruction *)
     2.5  fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
     2.6    let val thy = Proof_Context.theory_of ctxt
     2.7 +      val _ =
     2.8 +        if mode = FO then
     2.9 +          legacy_feature "Old 'metisF' command -- use 'metis' instead"
    2.10 +        else
    2.11 +          ()
    2.12        val new_skolemizer =
    2.13          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    2.14        val th_cls_pairs =