--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 13:55:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 14:05:22 2010 +0200
@@ -586,9 +586,8 @@
val local_facts = ProofContext.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static []
val is_chained = member Thm.eq_thm chained_ths
- (* Unnamed, not chained formulas with schematic variables are omitted,
- because they are rejected by the backticks (`...`) parser for some
- reason. *)
+ (* Unnamed nonchained formulas with schematic variables are omitted, because
+ they are rejected by the backticks (`...`) parser for some reason. *)
fun is_good_unnamed_local th =
forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))