src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 18797 8559cc115673
parent 18700 f04a8755d6ca
child 19046 bc5c6c9b114e
equal deleted inserted replaced
18796:5629fea8b4c6 18797:8559cc115673
   266 
   266 
   267 
   267 
   268 (*The signal handler in watcher.ML must be able to read the output of this.*)
   268 (*The signal handler in watcher.ML must be able to read the output of this.*)
   269 fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
   269 fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
   270  let val _ = trace
   270  let val _ = trace
   271                ("\nGetting lemma names. proofstr is " ^ proofstr ^
   271                ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
   272                 "\nprobfile is " ^ probfile ^
   272                 "\nprobfile is " ^ probfile ^
   273                 "  num of clauses is " ^ string_of_int (Array.length clause_arr))
   273                 "  num of clauses is " ^ string_of_int (Array.length clause_arr))
   274      val axiom_names = getax proofstr clause_arr
   274      val axiom_names = getax proofstr clause_arr
   275      val ax_str = rules_to_string axiom_names
   275      val ax_str = rules_to_string axiom_names
   276     in 
   276     in