author | kleing |
Sun, 29 Nov 2009 12:56:30 +1100 | |
changeset 33936 | 6e77ca6d3a8f |
parent 33935 | b94b4587106a |
child 33937 | b5ca587d0885 |
child 33938 | 7ed48b28bb7f |
child 33966 | b863967f23ea |
child 33988 | 901001414358 |
--- 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;