# HG changeset patch
# User blanchet
# Date 1391474148 -3600
# Node ID 54b0352fb46d10ef342e30b4f5c288ad1eba9954
# Parent  e0233567a8ef6b357206eacfe936a1e75f1d65ee
removed legacy 'metisFT' method

diff -r e0233567a8ef -r 54b0352fb46d NEWS
--- a/NEWS	Tue Feb 04 01:03:28 2014 +0100
+++ b/NEWS	Tue Feb 04 01:35:48 2014 +0100
@@ -122,6 +122,10 @@
       isar_try0 ~> try0_isar
     INCOMPATIBILITY.
 
+* Metis:
+  - Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead.
+    INCOMPATIBILITY.
+
 * Try0: Added 'algebra' and 'meson' to the set of proof methods.
 
 * The symbol "\<newline>" may be used within char or string literals
diff -r e0233567a8ef -r 54b0352fb46d src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Feb 04 01:03:28 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Feb 04 01:35:48 2014 +0100
@@ -262,11 +262,9 @@
 fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
   let
     val _ = trace_msg ctxt (fn () =>
-        "Metis called with theorems\n" ^
-        cat_lines (map (Display.string_of_thm ctxt) ths))
+      "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
     val type_encs = type_encs |> maps unalias_type_enc
-    fun tac clause =
-      resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
+    fun tac clause = resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
   in
     Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
   end
@@ -282,15 +280,10 @@
 val has_tvar =
   exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
 
-fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts =
+fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
   let
-    val _ =
-      if default_type_encs = full_type_encs then
-        legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
-      else
-        ()
     val (schem_facts, nonschem_facts) = List.partition has_tvar facts
-    val type_encs = override_type_encs |> the_default default_type_encs
+    val type_encs = override_type_encs |> the_default partial_type_encs
     val lam_trans = lam_trans |> the_default default_metis_lam_trans
   in
     HEADGOAL (Method.insert_tac nonschem_facts THEN'
@@ -301,8 +294,7 @@
 
 fun set_opt _ x NONE = SOME x
   | set_opt get x (SOME x0) =
-    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^
-           ".")
+    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^ ".")
 
 fun consider_opt s =
   if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
@@ -316,15 +308,9 @@
                            |> (case s' of SOME s' => consider_opt s' | _ => I)))
       (NONE, NONE)
 
-fun setup_method (binding, type_encs) =
-  Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo method type_encs)
-  |> Method.setup binding
-
 val setup =
-  [((@{binding metis}, partial_type_encs),
-    "Metis for FOL and HOL problems"),
-   ((@{binding metisFT}, full_type_encs),
-    "Metis for FOL/HOL problems with fully-typed translation")]
-  |> fold (uncurry setup_method)
+  Method.setup @{binding metis}
+    (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
+    "Metis for FOL and HOL problems"
 
 end;
diff -r e0233567a8ef -r 54b0352fb46d src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 01:03:28 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 01:35:48 2014 +0100
@@ -94,7 +94,7 @@
   Method.insert_tac local_facts THEN'
   (case meth of
     Metis_Method (type_enc_opt, lam_trans_opt) =>
-    Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_typesN]
+    Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
       (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
   | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
   | Meson_Method => Meson.meson_tac ctxt global_facts