# HG changeset patch
# User blanchet
# Date 1391115385 -3600
# Node ID daa64e603e70aaa73a135dec7ece22e6682d81d7
# Parent  78eb7fab3284cc98f3cd0af95a68751647f74b33
got rid of one of two Metis variants

diff -r 78eb7fab3284 -r daa64e603e70 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 30 21:56:25 2014 +0100
@@ -34,9 +34,10 @@
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
 
-fun preplay_trace ctxt assms concl result =
+fun preplay_trace ctxt assmsp concl result =
   let
     val ctxt = ctxt |> Config.put show_markup true
+    val assms = op @ assmsp
     val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
     val nr_of_assms = length assms
     val assms = assms
@@ -64,8 +65,7 @@
 fun resolve_fact_names ctxt names =
   (names
    |>> map string_of_label
-   |> op @
-   |> maps (thms_of_name ctxt))
+   |> pairself (maps (thms_of_name ctxt)))
   handle ERROR msg => error ("preplay error: " ^ msg)
 
 fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
@@ -86,15 +86,15 @@
     |> Skip_Proof.make_thm thy
   end
 
-fun tac_of_method meth type_enc lam_trans ctxt facts =
+fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
+  Method.insert_tac local_facts THEN'
   (case meth of
-    Metis_Method_with_Args => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
-  | Meson_Method => Meson.meson_tac ctxt facts
+    Meson_Method => Meson.meson_tac ctxt global_facts
+  | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
   | _ =>
-    Method.insert_tac facts THEN'
+    Method.insert_tac global_facts THEN'
     (case meth of
-      Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt []
-    | Simp_Method => Simplifier.asm_full_simp_tac ctxt
+      Simp_Method => Simplifier.asm_full_simp_tac ctxt
     | Simp_Size_Method =>
       Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
     | Auto_Method => K (Clasimp.auto_tac ctxt)
@@ -128,7 +128,10 @@
             Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
           end)
 
-      val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
+      val facts =
+        resolve_fact_names ctxt fact_names
+        |>> append (map (thm_of_proof ctxt) subproofs)
+
       val ctxt' = ctxt |> silence_reconstructors debug
 
       fun prove () =
diff -r 78eb7fab3284 -r daa64e603e70 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jan 30 21:56:25 2014 +0100
@@ -165,12 +165,19 @@
       | Meson_Method => "meson"
       | _ => raise Fail "Sledgehammer_Print: by_method")
 
-    fun using_facts [] [] = ""
-      | using_facts ls ss = "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
+    fun with_facts none _ [] [] = none
+      | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
+
+    val using_facts = with_facts "" (enclose "using " " ")
 
-    fun of_metis ls ss = reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
-
-    fun of_method ls ss Metis_Method_with_Args = of_metis ls ss
+    (* Local facts are always passed via "using", which affects "meson" and "metis". This is
+       arguably stylistically superior, because it emphasises the structure of the proof. It is also
+       more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
+       and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Preplay". *)
+    fun of_method ls ss Metis_Method =
+        using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ([], ss)
+      | of_method ls ss Meson_Method =
+        using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
       | of_method ls ss meth = using_facts ls ss ^ by_method meth
 
     fun of_byline ind (ls, ss) meth =
@@ -245,7 +252,7 @@
     (* One-step Metis proofs are pointless; better use the one-liner directly. *)
     (case proof of
       Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
-    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method_with_Args :: _) :: _))]) => ""
+    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
     | _ =>
       (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
       of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
diff -r 78eb7fab3284 -r daa64e603e70 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jan 30 21:56:25 2014 +0100
@@ -20,8 +20,8 @@
     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
       (facts * proof_method list list)
   and proof_method =
-    Metis_Method_with_Args | Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method |
-    Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
+    Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+    Arith_Method | Blast_Method | Meson_Method
 
   val no_label : label
   val no_facts : facts
@@ -69,8 +69,8 @@
   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
     (facts * proof_method list list)
 and proof_method =
-  Metis_Method_with_Args | Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method |
-  Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
+  Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+  Arith_Method | Blast_Method | Meson_Method
 
 val no_label = ("", ~1)
 val no_facts = ([],[])
diff -r 78eb7fab3284 -r daa64e603e70 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 21:56:25 2014 +0100
@@ -194,14 +194,14 @@
 
 val arith_methodss =
   [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
-    Metis_Method_with_Args], [Meson_Method]]
+    Metis_Method], [Meson_Method]]
 val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
 val metislike_methodss =
-  [[Metis_Method_with_Args, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+  [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
     Force_Method], [Meson_Method]]
 val rewrite_methodss =
-  [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method_with_Args], [Meson_Method]]
-val skolem_methodss = [[Metis_Method_with_Args, Blast_Method], [Metis_Method], [Meson_Method]]
+  [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
+val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
 
 fun isar_proof_text ctxt debug isar_proofs isar_params
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =