Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 28 Aug 2018 11:28:38 +0200
changeset 68828 7030922e91a1
parent 68827 1286ca9dfd26
child 68829 1a4fa494a4a8
tuned;
src/HOL/Real_Asymp/real_asymp_diag.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle