--- a/src/HOL/TPTP/ATP_Problem_Import.thy Sun Apr 22 14:16:46 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Sun Apr 22 14:16:46 2012 +0200
@@ -9,6 +9,8 @@
uses ("atp_problem_import.ML")
begin
+declare [[show_consts]] (* for Refute *)
+
typedecl iota (* for TPTP *)
use "atp_problem_import.ML"