# HG changeset patch
# User blanchet
# Date 1292508737 -3600
# Node ID 209546e0af2c8236979fd0efed9fed6c09bc17ef
# Parent  bd57cf5944cb492669daf2f9161d8a4ccaad5da2
comment tuning

diff -r bd57cf5944cb -r 209546e0af2c src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -270,8 +270,9 @@
        !skolem_cache)
     val flip = Option.map not
     (* We include free variables, as well as constants, to handle locales. For
-       each quantifiers that must necessarily be skolemized by the ATP, we
-       introduce a fresh constant to simulate the effect of Skolemization. *)
+       each quantifiers that must necessarily be skolemized by the automatic
+       prover, we introduce a fresh constant to simulate the effect of
+       Skolemization. *)
     fun do_const const x ts =
       (not (is_built_in_const x ts)
        ? add_pconst_to_table also_skolems (rich_pconst thy const x))
@@ -862,10 +863,6 @@
   List.partition (fst o snd) #> op @ #> map (apsnd snd)
   #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
 
-(***************************************************************)
-(* ATP invocation methods setup                                *)
-(***************************************************************)
-
 fun external_frees t =
   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)