# HG changeset patch
# User blanchet
# Date 1406757176 -7200
# Node ID 9df2757f5bec90381c31d4319e6d9459caaeeef9
# Parent  249f13fed1a6328c87763347b084f657507a31e6
tuned ML function name

diff -r 249f13fed1a6 -r 9df2757f5bec src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Wed Jul 30 23:52:56 2014 +0200
@@ -40,7 +40,7 @@
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
-        val gfs0 = filter (influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
+        val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
 
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
 
diff -r 249f13fed1a6 -r 9df2757f5bec src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed Jul 30 23:52:56 2014 +0200
@@ -36,7 +36,7 @@
   val is_proof_method_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
-  val influence_proof_method : Proof.context -> proof_method -> thm list -> bool
+  val thms_influence_proof_method : Proof.context -> proof_method -> thm list -> bool
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order
   val one_line_proof_text : Proof.context -> int -> one_line_params -> string
@@ -140,7 +140,7 @@
 val simp_based_methods =
   [Simp_Method, Simp_Size_Method, Auto_Method, Fastforce_Method, Force_Method]
 
-fun influence_proof_method ctxt meth ths =
+fun thms_influence_proof_method ctxt meth ths =
   not (member (op =) simp_based_methods meth) orelse
   let val ctxt' = silence_methods ctxt in
     (* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *)