src/HOL/Real_Asymp/multiseries_expansion.ML
changeset 69064 5840724b1d71
parent 68630 c55f6f0b3854
child 69597 ff784d5a5bfb
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML	Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML	Mon Sep 24 14:30:09 2018 +0200
@@ -2262,7 +2262,7 @@
       else if b aconv @{term "\<lambda>_::real. -1 :: real"} then
         Term.betapply (@{term "\<lambda>(f::real\<Rightarrow>real) x. -f x"}, a)
       else
-        Abs ("x", @{typ real}, @{term "( *) :: real => _"} $
+        Abs ("x", @{typ real}, @{term "(*) :: real => _"} $
           (Term.betapply (a, Bound 0)) $ (Term.betapply (b, Bound 0)))
 
     fun mk_powr b e =