diff -r 8d61b0aa7a0d -r 1e341728bae9 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Sat Feb 01 18:42:46 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Sat Feb 01 20:46:19 2014 +0100
@@ -172,7 +172,7 @@
       |> get_overloaded ctxt
       |> Option.map (Const o rpair (Term.type_of t));
   in
-    Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [proc]
+    Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc]
   end;
 
 fun check ctxt =