dead code
authorpaulson
Thu, 28 Jul 2005 17:55:39 +0200
changeset 16955 93270c5f56f6
parent 16954 82d0a25c5a1d
child 16956 5b413c866593
dead code
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 *)