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