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