diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -308,7 +308,7 @@
   have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
     by (intro integrable_const_bound) auto
   
-  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+  define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
   have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
     unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
   
@@ -343,7 +343,7 @@
   have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
     by (intro integrable_const_bound) auto
   
-  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+  define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
   have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
     unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)