--- a/src/HOL/Library/FinFun.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/FinFun.thy Sat Oct 10 19:22:05 2015 +0200
@@ -76,7 +76,7 @@
definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
-typedef ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
+typedef ('a,'b) finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
morphisms finfun_apply Abs_finfun
proof -
have "\<exists>f. finite {x. f x \<noteq> undefined}"
@@ -1528,9 +1528,6 @@
text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
no_type_notation
- finfun ("(_ =>f /_)" [22, 21] 21)
-
-no_type_notation (xsymbols)
finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
no_notation