Expand nested abbreviations before applying dummy patterns.

--- a/src/Pure/Tools/find_theorems.ML	Sun Nov 29 17:44:44 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sun Nov 29 12:56:30 2009 +1100
@@ -42,7 +42,7 @@
       | _ => Consts.intern consts nm);
   in
     (case try (Consts.the_abbreviation consts) nm' of
-      SOME (_, rhs) => apply_dummies rhs
+      SOME (_, rhs) => apply_dummies (ProofContext.expand_abbrevs ctxt rhs)
     | NONE => ProofContext.read_term_pattern ctxt nm)
   end;