--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 18 13:37:53 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 18 13:46:24 2012 +0200
@@ -486,19 +486,6 @@
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
-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
-
in
fun run_sledgehammer trivial args reconstructor named_thms id
@@ -544,7 +531,8 @@
SH_OK (time_isa, time_prover, names) =>
let
fun get_thms (name, stature) =
- try (thms_of_name (Proof.context_of st)) name
+ try (Sledgehammer_Reconstruct.thms_of_name (Proof.context_of st))
+ name
|> Option.map (pair (name, stature))
in
change_data id inc_sh_success;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 13:37:53 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 13:46:24 2012 +0200
@@ -28,6 +28,7 @@
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 :
@@ -59,6 +60,7 @@
open String_Redirect
+
(** reconstructors **)
datatype reconstructor =
@@ -76,6 +78,19 @@
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 **)
@@ -769,7 +784,7 @@
val facts =
fact_names
|>> map string_for_label |> op @
- |> map (Proof_Context.get_thm rich_ctxt)
+ |> map (the_single o thms_of_name rich_ctxt)
|> (if member (op =) qs Then then cons (the s0 |> thmify) else I)
val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t)
fun tac {context = ctxt, prems = _} =