src/HOL/TPTP/MaSh_Export.thy

--- a/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 13:32:13 2014 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 13:42:47 2014 +0100
@@ -29,7 +29,7 @@
 ML {*
 val do_it = false (* switch to "true" to generate the files *)
 val thys = [@{theory List}]
-val params as {provers, ...} = Sledgehammer_Commands.default_params @{context} []
+val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
 val prover = hd provers
 val range = (1, NONE)
 val step = 1