--- 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.
--- 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 =