# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1499721714 -7200
# Node ID 466d8e7ed1706a41773e5a84ada99eeaf6afeef8
# Parent  4a2c9d32e7aaea33b9708ee252488e0cc3000edf
FSet is monadic

diff -r 4a2c9d32e7aa -r 466d8e7ed170 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Mon Jul 10 18:53:38 2017 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Mon Jul 10 23:21:54 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Monad notation for arbitrary types\<close>
 
 theory Monad_Syntax
-imports Main "~~/src/Tools/Adhoc_Overloading"
+imports FSet "~~/src/Tools/Adhoc_Overloading"
 begin
 
 text \<open>
@@ -61,6 +61,6 @@
   "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
 
 adhoc_overloading
-  bind Set.bind Predicate.bind Option.bind List.bind
+  bind Set.bind Predicate.bind Option.bind List.bind FSet.fbind
 
-end
+end
\ No newline at end of file