1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 16:24:11 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 16:43:52 2010 +0200
     1.3 @@ -536,18 +536,23 @@
     1.4  
     1.5  fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
     1.6    let
     1.7 -    val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     1.8 +    val is_chained = member Thm.eq_thm chained_ths
     1.9 +    fun is_bad_unnamed_local th =
    1.10 +      exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
    1.11 +      (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
    1.12 +    val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
    1.13      val local_facts = ProofContext.facts_of ctxt
    1.14      val named_locals = local_facts |> Facts.dest_static []
    1.15 +    (* Unnamed, not chained formulas with schematic variables are omitted,
    1.16 +       because they are rejected by the backticks (`...`) parser for some
    1.17 +       reason. *)
    1.18      val unnamed_locals =
    1.19 -      local_facts |> Facts.props
    1.20 -      |> filter_out (fn th => exists (fn (_, ths) => member Thm.eq_thm ths th)
    1.21 -                                     named_locals)
    1.22 -      |> map (pair "" o single)
    1.23 +      local_facts |> Facts.props |> filter_out is_bad_unnamed_local
    1.24 +                  |> map (pair "" o single)
    1.25      val full_space =
    1.26        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
    1.27 -    fun add_valid_facts xfold facts =
    1.28 -      xfold (fn (name, ths0) =>
    1.29 +    fun add_valid_facts foldx facts =
    1.30 +      foldx (fn (name, ths0) =>
    1.31          if name <> "" andalso
    1.32             forall (not o member Thm.eq_thm add_thms) ths0 andalso
    1.33             (Facts.is_concealed facts name orelse
    1.34 @@ -577,8 +582,8 @@
    1.35              if name' = "" then
    1.36                I
    1.37              else
    1.38 -              cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
    1.39 -                             ? prefix chained_prefix, ths)
    1.40 +              cons (name' |> forall is_chained ths0 ? prefix chained_prefix,
    1.41 +                    ths)
    1.42            end)
    1.43    in
    1.44      [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)