src/HOL/Tools/res_atp.ML
changeset 16475 8f3ba52a7937
parent 16357 f1275d2a1dee
child 16478 d0a1f6231e2f
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jun 20 15:54:39 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jun 20 15:55:44 2005 +0200
     1.3 @@ -146,13 +146,16 @@
     1.4  (* now passing in list of skolemized thms and list of sgterms to go with them *)
     1.5  fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = let
     1.6     val axfile = (File.platform_path axiom_file)
     1.7 -    val hypsfile = (File.platform_path hyps_file)
     1.8 -     val clasimpfile = (File.platform_path clasimp_file)
     1.9 -    val spass_home = getenv "SPASS_HOME"
    1.10 +   val hypsfile = (File.platform_path hyps_file)
    1.11 +   val clasimpfile = (File.platform_path clasimp_file)
    1.12 +   val spass_home = getenv "SPASS_HOME"
    1.13 +   val spass = spass_home ^ "/SPASS"
    1.14 +   val _ = if File.exists (File.unpack_platform_path spass) then () 
    1.15 +	   else error ("Could not find the file " ^ spass)
    1.16       
    1.17 -fun make_atp_list [] sign n = []
    1.18 -|   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    1.19 -let 
    1.20 +   fun make_atp_list [] sign n = []
    1.21 +   |   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    1.22 +   let 
    1.23  	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
    1.24  	val thmproofstr = proofstring ( skothmstr)
    1.25  	val no_returns =List.filter   not_newline ( thmproofstr)