# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID c402981f74c178c69bc666d0cb3cca73c0522e1e
# Parent  12e1a5d8ee48811d003e495b371d13ba22e26304
use Skolem proof methods appropriately

diff -r 12e1a5d8ee48 -r c402981f74c1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -228,7 +228,8 @@
 
               val deps = fold add_fact_of_dependencies gamma no_facts
               val meths =
-                if is_arith_rule rule then arith_methods
+                if skolem then skolem_methods
+                else if is_arith_rule rule then arith_methods
                 else if is_datatype_rule rule then datatype_methods
                 else metislike_methods
               val by = (deps, meths)
@@ -238,7 +239,7 @@
                   [g] =>
                   if skolem andalso is_clause_tainted g then
                     let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
-                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methods)] infs
+                      isar_steps outer (SOME l) [prove [subproof] (no_facts, meths)] infs
                     end
                   else
                     do_rest l (prove [] by)