# HG changeset patch
# User wenzelm
# Date 1391283979 -3600
# Node ID 1e341728bae9dd42a83b3964d3ad47147c863c7d
# Parent  8d61b0aa7a0d44f49ae565fbf5d96cfdbea254ff
prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;

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 =