diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -33,7 +33,7 @@
   "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
 
 quotient_definition
-  "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" by auto
+  "(+) :: (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" by auto
 
 fun
   uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -78,7 +78,7 @@
 done
 
 quotient_definition
-  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+  "(( * )) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
   apply(rule equivp_transp[OF int_equivp])
   apply(rule times_int_raw_fst)
   apply(assumption)
@@ -92,7 +92,7 @@
   "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_definition
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" by auto
+  le_int_def: "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" by auto
 
 definition
   less_int_def: "(z::int) < w = (z \<le> w \<and> z \<noteq> w)"