# HG changeset patch
# User haftmann
# Date 1325878790 -3600
# Node ID c932c80d3eaeb38294dbdbd1fe93b4b7ea422365
# Parent  94479a979129fd3ea57dcd2dd9947733f31d6a14
farewell to theory More_List

diff -r 94479a979129 -r c932c80d3eae src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/IsaMakefile	Fri Jan 06 20:39:50 2012 +0100
@@ -286,7 +286,6 @@
   List.thy \
   Main.thy \
   Map.thy \
-  More_List.thy \
   More_Set.thy \
   Nat_Numeral.thy \
   Nat_Transfer.thy \
diff -r 94479a979129 -r c932c80d3eae src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Fri Jan 06 20:39:50 2012 +0100
@@ -74,7 +74,7 @@
   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
-  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
+  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
 *}
 
 end
diff -r 94479a979129 -r c932c80d3eae src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/List.thy	Fri Jan 06 20:39:50 2012 +0100
@@ -5109,6 +5109,19 @@
 by (induct xs) force+
 
 
+subsection {* Monad operation *}
+
+definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
+  "bind xs f = concat (map f xs)"
+
+hide_const (open) bind
+
+lemma bind_simps [simp]:
+  "List.bind [] f = []"
+  "List.bind (x # xs) f = f x @ List.bind xs f"
+  by (simp_all add: bind_def)
+
+
 subsection {* Transfer *}
 
 definition
diff -r 94479a979129 -r c932c80d3eae src/HOL/More_List.thy
--- a/src/HOL/More_List.thy	Fri Jan 06 11:15:02 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Author:  Florian Haftmann, TU Muenchen *)
-
-header {* Operations on lists beyond the standard List theory *}
-
-theory More_List
-imports List
-begin
-
-text {* monad operation *}
-
-definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
-  "bind xs f = concat (map f xs)"
-
-lemma bind_simps [simp]:
-  "bind [] f = []"
-  "bind (x # xs) f = f x @ bind xs f"
-  by (simp_all add: bind_def)
-
-end
diff -r 94479a979129 -r c932c80d3eae src/HOL/More_Set.thy
--- a/src/HOL/More_Set.thy	Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/More_Set.thy	Fri Jan 06 20:39:50 2012 +0100
@@ -4,7 +4,7 @@
 header {* Relating (finite) sets and lists *}
 
 theory More_Set
-imports More_List
+imports List
 begin
 
 lemma comp_fun_idem_remove: