# HG changeset patch
# User wenzelm
# Date 1535448518 -7200
# Node ID 7030922e91a11f19f85c19d0cbaf1830ca9f642f
# Parent  1286ca9dfd267b26c4310d498a42424efb7fd8d6
tuned;

diff -r 1286ca9dfd26 -r 7030922e91a1 src/HOL/Real_Asymp/real_asymp_diag.ML
--- a/src/HOL/Real_Asymp/real_asymp_diag.ML	Tue Aug 28 11:22:04 2018 +0200
+++ b/src/HOL/Real_Asymp/real_asymp_diag.ML	Tue Aug 28 11:28:38 2018 +0200
@@ -187,7 +187,7 @@
   end
 
 fun print_basis_elem ctxt t =
-  Syntax.pretty_term (Config.put Syntax_Trans.eta_contract_raw (Config.Bool false) ctxt)
+  Syntax.pretty_term (Config.put Syntax_Trans.eta_contract false ctxt)
     (Envir.eta_long [] t)
 
 val expansion_cmd =