src/HOL/Tools/ATP/atp_reconstruct.ML

     -> string proof -> (string * locality) list
   val used_facts_in_unsound_atp_proof :
     Proof.context -> type_sys -> int list list -> int
     -> (string * locality) list vector -> 'a proof -> string list option
   val uses_typed_helpers : int list -> 'a proof -> bool
-  val reconstructor_name : reconstructor -> string
   val one_line_proof_text : one_line_params -> string
   val make_tvar : string -> typ
   val make_tfree : Proof.context -> string -> typ
   val term_from_atp :
     Proof.context -> bool -> int Symtab.table -> typ option -> string fo_term

 
 
 (** Soft-core proof reconstruction: Metis one-liner **)
 
 (* unfortunate leaking abstraction *)
-fun reconstructor_name Metis = "metis"
-  | reconstructor_name Metis_Full_Types = "metis (full_types)"
-  | reconstructor_name Metis_No_Types = "metis (no_types)"
-  | reconstructor_name (SMT _) = "smt"
+fun name_of_reconstructor Metis = "metis"
+  | name_of_reconstructor Metis_Full_Types = "metis (full_types)"
+  | name_of_reconstructor Metis_No_Types = "metis (no_types)"
+  | name_of_reconstructor (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings
   | reconstructor_settings _ = ""
 
 fun string_for_label (s, num) = s ^ string_of_int num

   | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
 fun reconstructor_command reconstructor i n (ls, ss) =
   using_labels ls ^
   apply_on_subgoal (reconstructor_settings reconstructor) i n ^
-  command_call (reconstructor_name reconstructor) ss
+  command_call (name_of_reconstructor reconstructor) ss
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of
       "" => ""
     | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "."