diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -183,7 +183,7 @@
   {
     fix b
     assume "b \<in> as"
-    hence id2: "insert a as - {b} = insert a (as - {b})" using `a \<notin> as` by auto
+    hence id2: "insert a as - {b} = insert a (as - {b})" using \<open>a \<notin> as\<close> by auto
     have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
       unfolding id2
       by (subst setprod.insert, insert insert, auto)