src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Oct 22 20:08:25 2019 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Oct 22 20:55:13 2019 +0200
@@ -322,15 +322,6 @@
 \<close>
 
 ML \<open>
-val axms_of_thy =
-  `Theory.axioms_of
-  #> apsnd cterm_of
-  #> swap
-  #> apsnd (map snd)
-  #> uncurry map
-\<close>
-
-ML \<open>
 (*Show the skeleton-level inference which is done by each element of just_the_tacs. This is useful when debugging using the technique shown next*)
 if test_all @{context} orelse prob_names = [] then ()
 else