199 val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) |
199 val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) |
200 (*FIXME: hack!! need to consider relevance for all prems*) |
200 (*FIXME: hack!! need to consider relevance for all prems*) |
201 val _ = debug ("claset and simprules total clauses = " ^ |
201 val _ = debug ("claset and simprules total clauses = " ^ |
202 string_of_int (Array.length clause_arr)) |
202 string_of_int (Array.length clause_arr)) |
203 val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr) |
203 val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr) |
204 val pid_string = |
|
205 string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid))) |
|
206 in |
204 in |
207 debug ("initial thms: " ^ thms_string); |
205 debug ("initial thms: " ^ thms_string); |
208 debug ("subgoals: " ^ prems_string); |
206 debug ("subgoals: " ^ prems_string); |
209 debug ("pid: "^ pid_string); |
207 debug ("pid: " ^ Int.toString (ResLib.intOfPid pid)); |
210 write_problem_files axclauses thm (length prems); |
208 write_problem_files axclauses thm (length prems); |
211 watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid) |
209 watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid) |
212 end); |
210 end); |
213 |
211 |
214 val isar_atp_writeonly = setmp print_mode [] |
212 val isar_atp_writeonly = setmp print_mode [] |