equal
deleted
inserted
replaced
119 |
119 |
120 val spliteqs = warn_if_redundant ctxt feqs |
120 val spliteqs = warn_if_redundant ctxt feqs |
121 (Function_Split.split_all_equations ctxt compleqs) |
121 (Function_Split.split_all_equations ctxt compleqs) |
122 |
122 |
123 fun restore_spec thms = |
123 fun restore_spec thms = |
124 bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms) |
124 bnds ~~ (uncurry take) (length bnds, Library.unflat spliteqs thms) |
125 |
125 |
126 val spliteqs' = flat (Library.take (length bnds, spliteqs)) |
126 val spliteqs' = flat ((uncurry take) (length bnds, spliteqs)) |
127 val fnames = map (fst o fst) fixes |
127 val fnames = map (fst o fst) fixes |
128 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' |
128 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' |
129 |
129 |
130 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |
130 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |
131 |> map (map snd) |
131 |> map (map snd) |