# HG changeset patch
# User blanchet
# Date 1282661032 -7200
# Node ID 9bbd5141d0a154a9a11de5183a6d1128e7d795a6
# Parent  4c6b65d6a1354322a4dcb993decc71aec03ac5db
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)

diff -r 4c6b65d6a135 -r 9bbd5141d0a1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 16:24:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 16:43:52 2010 +0200
@@ -536,18 +536,23 @@
 
 fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
   let
-    val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
+    val is_chained = member Thm.eq_thm chained_ths
+    fun is_bad_unnamed_local th =
+      exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
+      (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
+    val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
     val local_facts = ProofContext.facts_of ctxt
     val named_locals = local_facts |> Facts.dest_static []
+    (* Unnamed, not chained formulas with schematic variables are omitted,
+       because they are rejected by the backticks (`...`) parser for some
+       reason. *)
     val unnamed_locals =
-      local_facts |> Facts.props
-      |> filter_out (fn th => exists (fn (_, ths) => member Thm.eq_thm ths th)
-                                     named_locals)
-      |> map (pair "" o single)
+      local_facts |> Facts.props |> filter_out is_bad_unnamed_local
+                  |> map (pair "" o single)
     val full_space =
       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
-    fun add_valid_facts xfold facts =
-      xfold (fn (name, ths0) =>
+    fun add_valid_facts foldx facts =
+      foldx (fn (name, ths0) =>
         if name <> "" andalso
            forall (not o member Thm.eq_thm add_thms) ths0 andalso
            (Facts.is_concealed facts name orelse
@@ -577,8 +582,8 @@
             if name' = "" then
               I
             else
-              cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
-                             ? prefix chained_prefix, ths)
+              cons (name' |> forall is_chained ths0 ? prefix chained_prefix,
+                    ths)
           end)
   in
     [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)