changeset 33939 | 7fc1ab75b4fa |
parent 33902 | 6e77ca6d3a8f |
child 33954 | fff6f11b1f09 |
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