--- a/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200
@@ -39,7 +39,7 @@
val path = file_name |> Path.explode
val lines = path |> File.read_lines
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts = all_facts_of thy css_table
+ val facts = all_facts_of (Proof_Context.init_global thy) css_table
val all_names = all_names (facts |> map snd)
val mepo_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0