# HG changeset patch
# User blanchet
# Date 1391085508 -3600
# Node ID d187a9908e8480fe5f5970adc87f7f11e84cb3e4
# Parent  56c0d70127a9b9162ee765e2df5be832eeef350a
'using' already uses the new Skolemizer, enabling a subtly shorter syntax

diff -r 56c0d70127a9 -r d187a9908e84 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 30 13:31:56 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 30 13:38:28 2014 +0100
@@ -89,14 +89,12 @@
 fun tac_of_method meth type_enc lam_trans ctxt facts =
   (case meth of
     Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
-  | Metis_New_Skolem_Method =>
-    tac_of_method Metis_Method type_enc lam_trans (Config.put Metis_Tactic.new_skolem true ctxt)
-      facts
   | Meson_Method => Meson.meson_tac ctxt facts
   | _ =>
     Method.insert_tac facts THEN'
     (case meth of
-      Simp_Method => Simplifier.asm_full_simp_tac ctxt
+      Metis_New_Skolem_Method => Metis_Tactic.metis_tac [type_enc] lam_trans 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)
diff -r 56c0d70127a9 -r d187a9908e84 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jan 30 13:31:56 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jan 30 13:38:28 2014 +0100
@@ -171,7 +171,6 @@
     fun of_metis ls ss = reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
 
     fun of_method ls ss Metis_Method = of_metis ls ss
-      | of_method ls ss Metis_New_Skolem_Method = "using [[metis_new_skolem]] " ^ of_metis ls ss
       | of_method ls ss meth = using_facts ls ss ^ by_method meth
 
     fun of_byline ind (ls, ss) meth =