# HG changeset patch
# User wenzelm
# Date 1256421653 -7200
# Node ID e3463e6db704b5d18c072d48595cfe2dda72e67a
# Parent  8846318b52d08d30a11cfd3198fe1dba7566027d
adapted Function_Lib (cf. b8cdd3d73022);

diff -r 8846318b52d0 -r e3463e6db704 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Oct 24 20:47:10 2009 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Oct 25 00:00:53 2009 +0200
@@ -1607,7 +1607,7 @@
       rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
 
   val regroup_munion_conv =
-      FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+      Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
         (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
 
   fun unfold_pwleq_tac i =
diff -r 8846318b52d0 -r e3463e6db704 src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Sat Oct 24 20:47:10 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML	Sun Oct 25 00:00:53 2009 +0200
@@ -112,7 +112,7 @@
     end
 
 fun bind_many [] = I
-  | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
+  | bind_many vs = Function_Lib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
 
 (* Builds relation descriptions from a relation definition *)
 fun mk_reldescs (Abs a) =