diff -r 1c6031e5d284 -r 4dd63cf5bba5 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 10:45:23 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 10:54:13 2013 +0100
@@ -38,7 +38,6 @@
   type step_name = string * string list
 
   datatype 'a step =
-    Definition_Step of step_name * 'a * 'a |
     Inference_Step of step_name * formula_role * 'a * string * step_name list
 
   type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
@@ -211,13 +210,11 @@
   end
 
 datatype 'a step =
-  Definition_Step of step_name * 'a * 'a |
   Inference_Step of step_name * formula_role * 'a * string * step_name list
 
 type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
 
-fun step_name (Definition_Step (name, _, _)) = name
-  | step_name (Inference_Step (name, _, _, _, _)) = name
+fun step_name (Inference_Step (name, _, _, _, _)) = name
 
 (**** PARSING OF TSTP FORMAT ****)
 
@@ -427,9 +424,7 @@
             case role_of_tptp_string role of
               Definition =>
               (case phi of
-                 AConn (AIff, [phi1 as AAtom _, phi2]) =>
-                 Definition_Step (name, phi1, phi2)
-               | AAtom (ATerm (("equal", []), _)) =>
+                 AAtom (ATerm (("equal", []), _)) =>
                  (* Vampire's equality proxy axiom *)
                  Inference_Step (name, Definition, phi, rule,
                                  map (rpair []) deps)
@@ -516,9 +511,6 @@
 
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen
-                          ((step as Definition_Step (name, _, _)) :: steps) =
-    step :: clean_up_dependencies (name :: seen) steps
-  | clean_up_dependencies seen
         (Inference_Step (name, role, u, rule, deps) :: steps) =
     Inference_Step (name, role, u, rule,
         map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
@@ -533,9 +525,7 @@
         AQuant (q, map (apfst f) xs, do_formula phi)
       | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
       | do_formula (AAtom t) = AAtom (do_term t)
-    fun do_step (Definition_Step (name, phi1, phi2)) =
-        Definition_Step (name, do_formula phi1, do_formula phi2)
-      | do_step (Inference_Step (name, role, phi, rule, deps)) =
+    fun do_step (Inference_Step (name, role, phi, rule, deps)) =
         Inference_Step (name, role, do_formula phi, rule, deps)
   in map do_step end