502 val pure_keywords = |
502 val pure_keywords = |
503 ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<", |
503 ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<", |
504 "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="]; |
504 "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="]; |
505 |
505 |
506 val pure_sections = |
506 val pure_sections = |
507 [section "classes" "|> add_classes" class_decls, |
507 [section "oracle" "|> set_oracle" ident, |
|
508 section "classes" "|> add_classes" class_decls, |
508 section "default" "|> add_defsort" sort, |
509 section "default" "|> add_defsort" sort, |
509 section "types" "" type_decls, |
510 section "types" "" type_decls, |
510 section "arities" "|> add_arities" arity_decls, |
511 section "arities" "|> add_arities" arity_decls, |
511 section "consts" "|> add_consts" const_decls, |
512 section "consts" "|> add_consts" const_decls, |
512 section "syntax" "|> add_syntax" const_decls, |
513 section "syntax" "|> add_syntax" const_decls, |