# HG changeset patch
# User kleing
# Date 1259459790 -39600
# Node ID 7fc1ab75b4fae08fe5aa9784ceb9fd04a7f0bb74
# Parent  639eb84ec640a22a2ce34b9f9a3d0040e8facf6c
Expand nested abbreviations before applying dummy patterns.

diff -r 639eb84ec640 -r 7fc1ab75b4fa src/Pure/Tools/find_theorems.ML
--- 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;