src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Nov 11 19:56:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 12 11:32:22 2012 +0100
@@ -188,7 +188,7 @@
       | NONE => hint
     end
   else
-    backquote_thm th
+    backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
 
 fun suggested_facts suggs facts =
   let