# HG changeset patch
# User blanchet
# Date 1399990696 -7200
# Node ID 4fca7e1470e2bcefe1a59dfc68eda48cb902ea34
# Parent  c49edf06f8e4f822cc4feb73d2b2b90fcf9f46b7
transfer theorems since 'silence_methods' may change the theory

diff -r c49edf06f8e4 -r 4fca7e1470e2 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue May 13 11:35:51 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue May 13 16:18:16 2014 +0200
@@ -90,14 +90,17 @@
   | Presburger_Method => "presburger"
   | Algebra_Method => "algebra")
 
-(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
-   exceeded" warnings and the like. *)
 fun silence_proof_methods debug =
   Try0.silence_methods debug
   #> Config.put SMT2_Config.verbose debug
 
-fun tac_of_proof_method ctxt0 debug (local_facts, global_facts) meth =
-  let val ctxt = silence_proof_methods debug ctxt0 in
+fun tac_of_proof_method ctxt0 debug (local_facts0, global_facts0) meth =
+  let
+    val ctxt = silence_proof_methods debug ctxt0
+    val thy = Proof_Context.theory_of ctxt
+    val local_facts = map (Thm.transfer thy) local_facts0
+    val global_facts = map (Thm.transfer thy) global_facts0
+  in
     Method.insert_tac local_facts THEN'
     (case meth of
       Metis_Method (type_enc_opt, lam_trans_opt) =>