src/HOL/Tools/Function/fun.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 34232 36a2a3029fd3
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Tue Nov 24 17:28:44 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Wed Nov 25 09:13:46 2009 +0100
     1.3 @@ -121,9 +121,9 @@
     1.4                             (Function_Split.split_all_equations ctxt compleqs)
     1.5  
     1.6            fun restore_spec thms =
     1.7 -              bnds ~~ (uncurry take) (length bnds, Library.unflat spliteqs thms)
     1.8 +              bnds ~~ take (length bnds) (unflat spliteqs thms)
     1.9                
    1.10 -          val spliteqs' = flat ((uncurry take) (length bnds, spliteqs))
    1.11 +          val spliteqs' = flat (take (length bnds) spliteqs)
    1.12            val fnames = map (fst o fst) fixes
    1.13            val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
    1.14