equal
deleted
inserted
replaced
196 (* @end *) |
196 (* @end *) |
197 |
197 |
198 (* @chunk read_specification *) |
198 (* @chunk read_specification *) |
199 fun read_specification' vars specs lthy = |
199 fun read_specification' vars specs lthy = |
200 let |
200 let |
201 val specs' = map (fn (a, s) => [(a, [s])]) specs |
201 val specs' = map (fn (a, s) => (a, [s])) specs |
202 val ((varst, specst), _) = |
202 val ((varst, specst), _) = |
203 Specification.read_specification vars specs' lthy |
203 Specification.read_specification vars specs' lthy |
204 val specst' = map (apsnd the_single) specst |
204 val specst' = map (apsnd the_single) specst |
205 in |
205 in |
206 (varst, specst') |
206 (varst, specst') |