1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -228,7 +228,8 @@
     1.4  
     1.5                val deps = fold add_fact_of_dependencies gamma no_facts
     1.6                val meths =
     1.7 -                if is_arith_rule rule then arith_methods
     1.8 +                if skolem then skolem_methods
     1.9 +                else if is_arith_rule rule then arith_methods
    1.10                  else if is_datatype_rule rule then datatype_methods
    1.11                  else metislike_methods
    1.12                val by = (deps, meths)
    1.13 @@ -238,7 +239,7 @@
    1.14                    [g] =>
    1.15                    if skolem andalso is_clause_tainted g then
    1.16                      let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
    1.17 -                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methods)] infs
    1.18 +                      isar_steps outer (SOME l) [prove [subproof] (no_facts, meths)] infs
    1.19                      end
    1.20                    else
    1.21                      do_rest l (prove [] by)