changeset 33936 | 6e77ca6d3a8f |
parent 33382 | 7d2c6e7f91bd |
child 33955 | fff6f11b1f09 |
--- 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;