src/HOL/Tools/res_atp.ML
changeset 15782 a1863ea9052b
parent 15779 aed221aff642
child 15919 b30a35432f5a
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Apr 20 17:19:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Apr 20 18:01:50 2005 +0200
     1.3 @@ -291,8 +291,8 @@
     1.4          val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
     1.5          (* set up variables for writing out the clasimps to a tptp file *)
     1.6  
     1.7 -        (* val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr*)
     1.8 -        (*val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  *)
     1.9 +         val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr
    1.10 +        val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
    1.11          (* cq: add write out clasimps to file *)
    1.12          (* cq:create watcher and pass to isar_atp_aux *) 
    1.13          (*val tenth_ax = fst( Array.sub(clause_arr, 10))