src/Pure/Tools/find_theorems.ML
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