--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 10:46:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 11:04:17 2011 +0200
@@ -42,7 +42,6 @@
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
@@ -254,10 +253,10 @@
(** 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 _ = ""
@@ -283,7 +282,7 @@
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