# HG changeset patch
# User blanchet
# Date 1392572382 -3600
# Node ID f6fc6d5339f1df86ddd3cc534f980c4bae1c5589
# Parent  8a54bf4a92cadb153c7f97f91704a8e6289c89b0
tuned code

diff -r 8a54bf4a92ca -r f6fc6d5339f1 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Sun Feb 16 18:39:41 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sun Feb 16 18:39:42 2014 +0100
@@ -259,8 +259,9 @@
    else
      all_tac) st0
 
-fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
+fun metis_tac type_encs0 lam_trans ctxt ths i st0 =
   let
+    val type_encs = if null type_encs0 then partial_type_encs else type_encs0
     val _ = trace_msg ctxt (fn () =>
       "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
     val type_encs = type_encs |> maps unalias_type_enc
@@ -269,25 +270,17 @@
     Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
   end
 
-fun metis_tac [] = generic_metis_tac partial_type_encs
-  | metis_tac type_encs = generic_metis_tac type_encs
-
-(* Whenever "X" has schematic type variables, we treat "using X by metis" as
-   "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
-   We don't do it for nonschematic facts "X" because this breaks a few proofs
-   (in the rare and subtle case where a proof relied on extensionality not being
-   applied) and brings few benefits. *)
-val has_tvar =
-  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
+(* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to
+   prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts
+   "X" because this breaks a few proofs (in the rare and subtle case where a proof relied on
+   extensionality not being applied) and brings few benefits. *)
+val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
 
 fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
-  let
-    val (schem_facts, nonschem_facts) = List.partition has_tvar facts
-    val type_encs = override_type_encs |> the_default partial_type_encs
-    val lam_trans = lam_trans |> the_default default_metis_lam_trans
-  in
+  let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
     HEADGOAL (Method.insert_tac nonschem_facts THEN'
-      CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt (schem_facts @ ths))
+      CHANGED_PROP o metis_tac (these override_type_encs)
+        (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
   end
 
 val metis_lam_transs = [hide_lamsN, liftingN, combsN]