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