src/HOL/Tools/ATP/watcher.ML
changeset 17315 5bf0e0aacc24
parent 17306 5cde710a8a23
child 17317 3f12de2e2e6e
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 08 16:09:23 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 08 17:35:02 2005 +0200
     1.3 @@ -434,7 +434,7 @@
     1.4  			      prems_string^prover^thmstring^goalstring^childCmd) 
     1.5  		       val childDone = (case prover of
     1.6  			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
     1.7 -			    | "E" => EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
     1.8 +			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
     1.9  			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
    1.10  		    in
    1.11  		     if childDone      (**********************************************)