src/Pure/Isar/overloading.ML

--- a/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -87,7 +87,7 @@
   end;
 
 fun rewrite_liberal thy unchecks t =
-  (case try (Pattern.rewrite_term thy unchecks []) t of
+  (case try (Pattern.rewrite_term_top thy unchecks []) t of
     NONE => NONE
   | SOME t' => if t aconv t' then NONE else SOME t');