diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Apr 12 11:08:25 2005 +0200
@@ -309,7 +309,7 @@
         val thmstring = string_of_thm thm
         val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
         (* set up variables for writing out the clasimps to a tptp file *)
-        (* val _ = write_out_clasimp (File.sysify_path axiom_file)*)
+        val _ = write_out_clasimp (File.sysify_path axiom_file)
         (* cq: add write out clasimps to file *)
         (* cq:create watcher and pass to isar_atp_aux *)                    
         val (childin,childout,pid) = Watcher.createWatcher()