--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 28 12:25:43 2012 +0100
@@ -531,7 +531,7 @@
SH_OK (time_isa, time_prover, names) =>
let
fun get_thms (name, stature) =
- try (Sledgehammer_Reconstruct.thms_of_name (Proof.context_of st))
+ try (Sledgehammer_Util.thms_of_name (Proof.context_of st))
name
|> Option.map (pair (name, stature))
in
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Nov 28 12:25:43 2012 +0100
@@ -53,19 +53,6 @@
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
end
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (Proof_Context.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover=SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
let val override_params = override_params @ [("preplay_timeout", "0")] in
case run_prover override_params fact_override i i ctxt th of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Nov 28 12:25:43 2012 +0100
@@ -30,19 +30,6 @@
fun string_for_label (s, num) = s ^ string_of_int num
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (Proof_Context.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover = SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
val inc = curry op+
fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0
fun metis_steps_recursive proof =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
@@ -28,7 +28,6 @@
val smtN : string
val string_for_reconstructor : reconstructor -> string
- val thms_of_name : Proof.context -> string -> thm list
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 :
@@ -82,19 +81,6 @@
metis_call type_enc lam_trans
| string_for_reconstructor SMT = smtN
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (Proof_Context.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover = SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
(** fact extraction from ATP proofs **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
@@ -111,7 +111,7 @@
fact_names
|>> map string_for_label
|> op @
- |> maps (thms_of_name ctxt) (* FIXME: maps (the o thms_of_name ctxt) *)
+ |> maps (thms_of_name ctxt)
val goal =
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
fun tac {context = ctxt, prems = _} =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 28 12:25:43 2012 +0100
@@ -18,6 +18,7 @@
val subgoal_count : Proof.state -> int
val reserved_isar_keyword_table : unit -> unit Symtab.table
val thms_in_proof : unit Symtab.table option -> thm -> string list
+ val thms_of_name : Proof.context -> string -> thm list
val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
end;
@@ -102,6 +103,19 @@
[] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
in names end
+fun thms_of_name ctxt name =
+ let
+ val lex = Keyword.get_lexicons
+ val get = maps (Proof_Context.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source
+ |> Token.source {do_recover = SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
fun with_vanilla_print_mode f x =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) f x