210 |
210 |
211 |
211 |
212 (** outer syntax **) |
212 (** outer syntax **) |
213 |
213 |
214 val domaindef_decl = |
214 val domaindef_decl = |
215 Scan.optional (Parse.$$$ "(" |-- |
215 Scan.optional (@{keyword "("} |-- |
216 ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding || |
216 ((@{keyword "open"} >> K false) -- Scan.option Parse.binding || |
217 Parse.binding >> (fn s => (true, SOME s))) |
217 Parse.binding >> (fn s => (true, SOME s))) |
218 --| Parse.$$$ ")") (true, NONE) -- |
218 --| @{keyword ")"}) (true, NONE) -- |
219 (Parse.type_args_constrained -- Parse.binding) -- |
219 (Parse.type_args_constrained -- Parse.binding) -- |
220 Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) -- |
220 Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) -- |
221 Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)) |
221 Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) |
222 |
222 |
223 fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) = |
223 fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) = |
224 domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) |
224 domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) |
225 |
225 |
226 val _ = |
226 val _ = |