| changeset 60472 | 53ba9ea403ad |
| parent 60470 | dab7b21673ee |
| child 60473 | 4c61bb3aa06d |
| 60471:37f4a25ec3a9 | 60472:53ba9ea403ad |
|---|---|
197 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_) |
197 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_) |
198 val pbt' = filter_out O_Model.is_copy_named pbt |
198 val pbt' = filter_out O_Model.is_copy_named pbt |
199 val cy = filter O_Model.is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *) |
199 val cy = filter O_Model.is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *) |
200 val oris' = matc thy pbt' ags [] |
200 val oris' = matc thy pbt' ags [] |
201 val cy' = map (O_Model.cpy_nam pbt' oris') cy |
201 val cy' = map (O_Model.cpy_nam pbt' oris') cy |
202 val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the Model-items *) |
202 val ors = O_Model.add_enumerate (oris' @ cy') (*...appended in order to get into the Model-items *) |
203 in (map flattup ors) end |
203 in (map flattup ors) end |
204 |
204 |
205 (* report part of the error-msg which is not available in match_args *) |
205 (* report part of the error-msg which is not available in match_args *) |
206 fun arguments_msg pI stac ags = |
206 fun arguments_msg pI stac ags = |
207 let |
207 let |