--- a/src/HOL/Tools/Function/fun.ML Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML Tue Nov 24 17:28:25 2009 +0100
@@ -121,9 +121,9 @@
(Function_Split.split_all_equations ctxt compleqs)
fun restore_spec thms =
- bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
+ bnds ~~ (uncurry take) (length bnds, Library.unflat spliteqs thms)
- val spliteqs' = flat (Library.take (length bnds, spliteqs))
+ val spliteqs' = flat ((uncurry take) (length bnds, spliteqs))
val fnames = map (fst o fst) fixes
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'