# HG changeset patch
# User kleing
# Date 1259459790 -39600
# Node ID 6e77ca6d3a8f8293d6799f1d319166481c36cb8e
# Parent  b94b4587106a44def26ad32f6ba361c66482abcf
Expand nested abbreviations before applying dummy patterns.

diff -r b94b4587106a -r 6e77ca6d3a8f src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Nov 27 16:26:23 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;