diff -r f9682fdfd47b -r 3858246c7c8f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Sep 12 10:40:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Sep 12 11:05:19 2013 +0200
@@ -452,7 +452,7 @@
 end
 
 fun mash_unlearn ctxt ({overlord, ...} : params) =
-  (clear_state ctxt overlord; Output.urgent_message "Reset MaSh")
+  (clear_state ctxt overlord; Output.urgent_message "Reset MaSh.")
 
 
 (*** Isabelle helpers ***)
@@ -951,14 +951,17 @@
   fold (fn s => Symtab.map_default (s, 0) (Integer.add 1))
        (Term.add_const_names t [])
 
-fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
-                         concl_t facts =
+fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) prover max_facts
+                         hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
+    val thy_name = Context.theory_name thy
     val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
     val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
     val num_facts = length facts
     val const_tab = fold (add_const_counts o prop_of o snd) facts Symtab.empty
+    fun fact_has_right_theory (_, th) =
+      thy_name = Context.theory_name (theory_of_thm th)
     fun chained_or_extra_features_of factor (((_, stature), th), weight) =
       [prop_of th]
       |> features_of ctxt prover (theory_of_thm th) num_facts const_tab stature
@@ -971,8 +974,8 @@
             let
               val parents = maximal_wrt_access_graph access_G facts
               val goal_feats =
-                features_of ctxt prover thy num_facts const_tab
-                            (Local, General) (concl_t :: hyp_ts)
+                features_of ctxt prover thy num_facts const_tab (Local, General)
+                            (concl_t :: hyp_ts)
               val chained_feats =
                 chained
                 |> map (rpair 1.0)
@@ -981,12 +984,14 @@
               val extra_feats =
                 facts
                 |> take (Int.max (0, num_extra_feature_facts - length chained))
+                |> filter fact_has_right_theory
                 |> weight_facts_steeply
                 |> map (chained_or_extra_features_of extra_feature_factor)
                 |> rpair [] |-> fold (union (eq_fst (op =)))
               val feats =
                 fold (union (eq_fst (op =))) [chained_feats, extra_feats]
                      goal_feats
+                |> debug ? sort (Real.compare o swap o pairself snd)
               val hints =
                 chained |> filter (is_fact_in_graph access_G o snd)
                         |> map (nickname_of_thm o snd)