# HG changeset patch
# User paulson
# Date 1122566139 -7200
# Node ID 93270c5f56f622cbf7309d76472222b6492372fa
# Parent  82d0a25c5a1d2de19da88408023b37fd360cb3b6
dead code

diff -r 82d0a25c5a1d -r 93270c5f56f6 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Jul 28 17:54:39 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Jul 28 17:55:39 2005 +0200
@@ -73,11 +73,6 @@
     String.translate (fn c => if is_proof_char c then str c else "");
 
 
-(*
-fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac);
-
-*)
-
 (**** For running in Isar ****)
 
 (* same function as that in res_axioms.ML *)