src/Tools/adhoc_overloading.ML

     fun proc t =
       Term.map_types (K dummyT) t
       |> 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 =
   map (fn t => Term.map_aterms (insert_variants ctxt t) t);