Use top-down rewriting to contract abbreviations.

--- a/src/Pure/Isar/proof_context.ML	Thu Feb 18 17:27:18 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Feb 18 17:28:02 2010 +0100
@@ -492,7 +492,7 @@
     fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
   in
     if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
-    else Pattern.rewrite_term thy [] [match_abbrev] t
+    else Pattern.rewrite_term_top thy [] [match_abbrev] t
   end;