# HG changeset patch
# User blanchet
# Date 1350560784 -7200
# Node ID 412346127bfa346ccee5a5347096a5bc3f0d652d
# Parent  e88a864fa35ce20a252db48ad2ab5edb3779883c
fixed theorem lookup code in Isar proof reconstruction

diff -r e88a864fa35c -r 412346127bfa src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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;
diff -r e88a864fa35c -r 412346127bfa src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 = _} =