Expand nested abbreviations before applying dummy patterns.
1.1 --- a/src/Pure/Tools/find_theorems.ML Sun Nov 29 17:44:44 2009 +0100
1.2 +++ b/src/Pure/Tools/find_theorems.ML Sun Nov 29 12:56:30 2009 +1100
1.3 @@ -42,7 +42,7 @@
1.4 | _ => Consts.intern consts nm);
1.5 in
1.6 (case try (Consts.the_abbreviation consts) nm' of
1.7 - SOME (_, rhs) => apply_dummies rhs
1.8 + SOME (_, rhs) => apply_dummies (ProofContext.expand_abbrevs ctxt rhs)
1.9 | NONE => ProofContext.read_term_pattern ctxt nm)
1.10 end;
1.11