--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 20 16:05:25 2010 +0200
@@ -708,7 +708,7 @@
fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
let
val thy = ProofContext.theory_of ctxt
- val global_facts = PureThy.facts_of thy
+ val global_facts = Global_Theory.facts_of thy
val local_facts = ProofContext.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static []
val assms = Assumption.all_assms_of ctxt