# HG changeset patch
# User berghofe
# Date 1266510482 -3600
# Node ID 5d2fe4e093541cc20e0689787d157e031fe8d923
# Parent  6e45e4c947516dfcffc1633fc0c5fcf4a0a5292a
Use top-down rewriting to contract abbreviations.

diff -r 6e45e4c94751 -r 5d2fe4e09354 src/Pure/Isar/proof_context.ML
--- 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;