bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;

--- a/NEWS	Fri Jun 10 22:47:25 2016 +0200
+++ b/NEWS	Fri Jun 10 23:13:04 2016 +0200
@@ -148,6 +148,11 @@
 
 * Probability/SPMF formalises discrete subprobability distributions.
 
+* Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax"
+allow to control optional syntax in local contexts; this supersedes
+former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle
+finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax".
+
 * Library/Set_Permutations.thy (executably) defines the set of 
 permutations of a set, i.e. the set of all lists that contain every 
 element of the carrier set exactly once.

--- 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

--- a/src/HOL/Library/FinFun_Syntax.thy	Fri Jun 10 22:47:25 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Author: Andreas Lochbihler, KIT *)
-
-section \<open>Pretty syntax for almost everywhere constant functions\<close>
-
-theory FinFun_Syntax
-imports FinFun
-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

--- a/src/HOL/ROOT	Fri Jun 10 22:47:25 2016 +0200
+++ b/src/HOL/ROOT	Fri Jun 10 23:13:04 2016 +0200
@@ -545,7 +545,6 @@
     Hebrew
     Chinese
     Serbian
-    "~~/src/HOL/Library/FinFun_Syntax"
     "~~/src/HOL/Library/Refute"
     "~~/src/HOL/Library/Transitive_Closure_Table"
     Cartouche_Examples

--- a/src/HOL/ex/FinFunPred.thy	Fri Jun 10 22:47:25 2016 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Fri Jun 10 23:13:04 2016 +0200
@@ -1,10 +1,12 @@
 (*  Author:     Andreas Lochbihler *)
 
-section \<open>
-  Predicates modelled as FinFuns
-\<close>
+section \<open>Predicates modelled as FinFuns\<close>
 
-theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin
+theory FinFunPred
+imports "~~/src/HOL/Library/FinFun"
+begin
+
+unbundle finfun_syntax
 
 text \<open>Instantiate FinFun predicates just like predicates\<close>