src/HOL/Tools/ATP/watcher.ML
changeset 17235 8e55ad29b690
parent 17234 12a9393c5d77
child 17305 6cef3aedd661
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 17:55:24 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 21:29:33 2005 +0200
     1.3 @@ -502,7 +502,8 @@
     1.4  				("subgoals forked to checkChildren:"^
     1.5  				prems_string^prover^thmstring^goalstring^childCmd) 
     1.6  			 val childDone = (case prover of
     1.7 -			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
     1.8 +			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )     
     1.9 +                              | "E" => (EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )              
    1.10  			    |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
    1.11  		      in
    1.12  		       if childDone      (**********************************************)