# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 831d28439b3a9bd5a000fa8fe5a824dd2d842f56
# Parent  23b81469499f0269a60f3b8314e42230774635fd
marked "metisF" as legacy -- nobody uses it or needs it

diff -r 23b81469499f -r 831d28439b3a NEWS
--- a/NEWS	Mon Jun 06 20:36:35 2011 +0200
+++ b/NEWS	Mon Jun 06 20:36:35 2011 +0200
@@ -85,6 +85,9 @@
     TPTP problems (TFF).
   - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
 
+* Metis:
+  - Obsoleted "metisF" -- use "metis" instead.
+
 * "try":
   - Added "simp:", "intro:", and "elim:" options.
 
diff -r 23b81469499f -r 831d28439b3a src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -93,6 +93,11 @@
 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
   let val thy = Proof_Context.theory_of ctxt
+      val _ =
+        if mode = FO then
+          legacy_feature "Old 'metisF' command -- use 'metis' instead"
+        else
+          ()
       val new_skolemizer =
         Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
       val th_cls_pairs =