Expand nested abbreviations before applying dummy patterns.
authorkleing
Sun, 29 Nov 2009 12:56:30 +1100
changeset 339397fc1ab75b4fa
parent 33938 639eb84ec640
child 33940 e1c262952b02
Expand nested abbreviations before applying dummy patterns.
src/Pure/Tools/find_theorems.ML
     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