src/HOL/Tools/ATP/atp_proof.ML

     UnknownError of string
 
   type step_name = string * string list
 
   datatype 'a step =
-    Definition of step_name * 'a * 'a |
-    Inference of step_name * 'a * string * step_name list
+    Definition_Step of step_name * 'a * 'a |
+    Inference_Step of step_name * 'a * string * step_name list
 
   type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
 
   val short_output : bool -> string -> string
   val string_for_failure : failure -> string

     | (SOME _, NONE) => GREATER
     | (SOME i, SOME j) => int_ord (i, j)
   end
 
 datatype 'a step =
-  Definition of step_name * 'a * 'a |
-  Inference of step_name * 'a * string * step_name list
+  Definition_Step of step_name * 'a * 'a |
+  Inference_Step of step_name * 'a * string * step_name list
 
 type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
 
-fun step_name (Definition (name, _, _)) = name
-  | step_name (Inference (name, _, _, _)) = name
+fun step_name (Definition_Step (name, _, _)) = name
+  | step_name (Inference_Step (name, _, _, _)) = name
 
 (**** PARSING OF TSTP FORMAT ****)
 
 (* FIXME: temporary hack *)
 fun repair_waldmeister_step_name s =

           in
             case role of
               "definition" =>
               (case phi of
                  AConn (AIff, [phi1 as AAtom _, phi2]) =>
-                 Definition (name, phi1, phi2)
+                 Definition_Step (name, phi1, phi2)
                | AAtom (ATerm ("equal", _)) =>
                  (* Vampire's equality proxy axiom *)
-                 Inference (name, phi, rule, map (rpair []) deps)
+                 Inference_Step (name, phi, rule, map (rpair []) deps)
                | _ => raise UNRECOGNIZED_ATP_PROOF ())
-            | _ => Inference (name, phi, rule, map (rpair []) deps)
+            | _ => Inference_Step (name, phi, rule, map (rpair []) deps)
           end)
 
 (**** PARSING OF SPASS OUTPUT ****)
 
 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role

     -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
     -- parse_horn_clause --| $$ "."
     -- Scan.option (Scan.this_string "derived from formulae "
                     |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
   >> (fn ((((num, rule), deps), u), names) =>
-         Inference ((num, resolve_spass_num names spass_names num), u, rule,
-                    map (swap o `(resolve_spass_num NONE spass_names)) deps))
+         Inference_Step ((num, resolve_spass_num names spass_names num), u,
+             rule, map (swap o `(resolve_spass_num NONE spass_names)) deps))
 
 (* Syntax: <name> *)
 fun parse_satallax_line x =
   (scan_general_id --| Scan.option ($$ " ")
-   >> (fn s => Inference ((s, [s]), dummy_phi, "", []))) x
+   >> (fn s => Inference_Step ((s, [s]), dummy_phi, "", []))) x
 
 fun parse_line problem spass_names =
   parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
 fun parse_proof problem spass_names tstp =
   tstp |> strip_spaces_except_between_idents

     tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
     |> parse_proof problem (extract_spass_name_vector output)
     |> sort (step_name_ord o pairself step_name)
 
 fun clean_up_dependencies _ [] = []
-  | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) =
+  | clean_up_dependencies seen
+                          ((step as Definition_Step (name, _, _)) :: steps) =
     step :: clean_up_dependencies (name :: seen) steps
-  | clean_up_dependencies seen (Inference (name, u, rule, deps) :: steps) =
-    Inference (name, u, rule,
-               map_filter (fn dep => find_first (is_same_atp_step dep) seen)
-                          deps) ::
+  | clean_up_dependencies seen (Inference_Step (name, u, rule, deps) :: steps) =
+    Inference_Step (name, u, rule,
+        map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
     clean_up_dependencies (name :: seen) steps
 
 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
 
 fun map_term_names_in_term f (ATerm (s, ts)) =

 fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
     AQuant (q, xs, map_term_names_in_formula f phi)
   | map_term_names_in_formula f (AConn (c, phis)) =
     AConn (c, map (map_term_names_in_formula f) phis)
   | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t)
-fun map_term_names_in_step f (Definition (name, phi1, phi2)) =
-    Definition (name, map_term_names_in_formula f phi1,
-                map_term_names_in_formula f phi2)
-  | map_term_names_in_step f (Inference (name, phi, rule, deps)) =
-    Inference (name, map_term_names_in_formula f phi, rule, deps)
+fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) =
+    Definition_Step (name, map_term_names_in_formula f phi1,
+                     map_term_names_in_formula f phi2)
+  | map_term_names_in_step f (Inference_Step (name, phi, rule, deps)) =
+    Inference_Step (name, map_term_names_in_formula f phi, rule, deps)
 fun map_term_names_in_atp_proof f = map (map_term_names_in_step f)
 
 fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
 fun nasty_atp_proof pool =
   if Symtab.is_empty pool then I