diff -r 7c509ddf29a5 -r a59801b7f125 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Fri Jun 10 22:47:25 2016 +0200
+++ b/src/HOL/Library/FinFun.thy	Fri Jun 10 23:13:04 2016 +0200
@@ -1534,14 +1534,38 @@
 instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
 end
 
-text \<open>Deactivate syntax again. Import theory \<open>FinFun_Syntax\<close> to reactivate it again\<close>
+
+subsubsection \<open>Bundles for concrete syntax\<close>
+
+bundle finfun_syntax
+begin
+
+type_notation finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
+
+notation
+  finfun_const ("K$/ _" [0] 1) and
+  finfun_update ("_'(_ $:= _')" [1000, 0, 0] 1000) and
+  finfun_apply (infixl "$" 999) and
+  finfun_comp (infixr "\<circ>$" 55) and
+  finfun_comp2 (infixr "$\<circ>" 55) and
+  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
+
+notation (ASCII)
+  finfun_comp (infixr "o$" 55) and
+  finfun_comp2 (infixr "$o" 55)
+
+end
+
+
+bundle no_finfun_syntax
+begin
 
 no_type_notation
   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
 
 no_notation
   finfun_const ("K$/ _" [0] 1) and
-  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
+  finfun_update ("_'(_ $:= _')" [1000, 0, 0] 1000) and
   finfun_apply (infixl "$" 999) and
   finfun_comp (infixr "\<circ>$" 55) and
   finfun_comp2 (infixr "$\<circ>" 55) and
@@ -1552,3 +1576,7 @@
   finfun_comp2 (infixr "$o" 55)
 
 end
+
+unbundle no_finfun_syntax
+
+end