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