src/HOL/Library/Monad_Syntax.thy
changeset 52622 e0ff1625e96d
parent 46143 c932c80d3eae
child 53616 ff37dc246b10
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Jul 12 15:51:25 2013 +0200
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Fri Jul 12 16:19:05 2013 +0200
     1.3 @@ -69,12 +69,7 @@
     1.4    "_do_block (_do_final e)" => "e"
     1.5    "(m >> n)" => "(m >>= (\<lambda>_. n))"
     1.6  
     1.7 -setup {*
     1.8 -  Adhoc_Overloading.add_overloaded @{const_name bind}
     1.9 -  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
    1.10 -  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
    1.11 -  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
    1.12 -  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
    1.13 -*}
    1.14 +adhoc_overloading
    1.15 +  bind Set.bind Predicate.bind Option.bind List.bind
    1.16  
    1.17  end