# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 1da2e67242d64ada79d8067f7082d2f4deefe6b6
# Parent  e8173d1fa725757584b50c30a7615984b430e891
moved thms_of_name to Sledgehammer_Util and removed copies, updated references

diff -r e8173d1fa725 -r 1da2e67242d6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
diff -r e8173d1fa725 -r 1da2e67242d6 src/HOL/TPTP/sledgehammer_tactics.ML
--- 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
diff -r e8173d1fa725 -r 1da2e67242d6 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- 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 = 
diff -r e8173d1fa725 -r 1da2e67242d6 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 **)
 
diff -r e8173d1fa725 -r 1da2e67242d6 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- 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 = _} =
diff -r e8173d1fa725 -r 1da2e67242d6 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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