--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed May 15 17:27:24 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed May 15 17:43:42 2013 +0200
@@ -27,7 +27,7 @@
* (string * stature) list vector * int Symtab.table * string proof * thm
val smtN : string
- val string_for_reconstructor : reconstructor -> string
+ val string_of_reconstructor : reconstructor -> string
val lam_trans_from_atp_proof : string proof -> string -> string
val is_typed_helper_used_in_atp_proof : string proof -> bool
val used_facts_in_atp_proof :
@@ -78,9 +78,9 @@
val smtN = "smt"
-fun string_for_reconstructor (Metis (type_enc, lam_trans)) =
+fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
metis_call type_enc lam_trans
- | string_for_reconstructor SMT = smtN
+ | string_of_reconstructor SMT = smtN
(** fact extraction from ATP proofs **)
@@ -207,7 +207,7 @@
fun using_labels [] = ""
| using_labels ls =
- "using " ^ space_implode " " (map string_for_label ls) ^ " "
+ "using " ^ space_implode " " (map string_of_label ls) ^ " "
fun command_call name [] =
name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
@@ -216,7 +216,7 @@
fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
(* unusing_chained_facts used_chaineds num_chained ^ *)
using_labels ls ^ apply_on_subgoal i n ^
- command_call (string_for_reconstructor reconstr) ss
+ command_call (string_of_reconstructor reconstr) ss
fun try_command_line banner time command =
banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
@@ -270,14 +270,14 @@
val have_prefix = "f"
val raw_prefix = "x"
-fun raw_label_for_name (num, ss) =
+fun raw_label_of_name (num, ss) =
case resolve_conjecture ss of
[j] => (conjecture_prefix, j)
| _ => (raw_prefix ^ ascii_of num, 0)
-fun label_of_clause [name] = raw_label_for_name name
+fun label_of_clause [name] = raw_label_of_name name
| label_of_clause c =
- (space_implode "___" (map (fst o raw_label_for_name) c), 0)
+ (space_implode "___" (map (fst o raw_label_of_name) c), 0)
fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
if is_fact fact_names ss then
@@ -425,13 +425,13 @@
val indent_size = 2
-fun string_for_proof ctxt type_enc lam_trans i n proof =
+fun string_of_proof ctxt type_enc lam_trans i n proof =
let
val register_fixes = map Free #> fold Variable.auto_fixes
fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
fun of_indent ind = replicate_string (ind * indent_size) " "
fun of_moreover ind = of_indent ind ^ "moreover\n"
- fun of_label l = if l = no_label then "" else string_for_label l ^ ": "
+ fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
fun of_obtain qs nr =
(if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
"ultimately "
@@ -558,7 +558,7 @@
Proof (fix, do_assms assms, map do_step steps)
in do_proof proof end
-fun prefix_for_depth n = replicate_string (n + 1)
+fun prefix_of_depth n = replicate_string (n + 1)
val relabel_proof =
let
@@ -566,7 +566,7 @@
if l = no_label then
old
else
- let val l' = (prefix_for_depth depth prefix, next) in
+ let val l' = (prefix_of_depth depth prefix, next) in
(l', (l, l') :: subst, next + 1)
end
fun do_facts subst =
@@ -677,7 +677,7 @@
(case resolve_conjecture ss of
[j] =>
if j = length hyp_ts then NONE
- else SOME (raw_label_for_name name, nth hyp_ts j)
+ else SOME (raw_label_of_name name, nth hyp_ts j)
| _ => NONE)
| _ => NONE)
val bot = atp_proof |> List.last |> #1
@@ -808,8 +808,8 @@
(if isar_proofs = SOME true then isar_compress else 1000.0))
|>> clean_up_labels_in_proof
val isar_text =
- string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
- isar_proof
+ string_of_proof ctxt type_enc lam_trans subgoal subgoal_count
+ isar_proof
in
case isar_text of
"" =>