equal
deleted
inserted
replaced
624 ) >> (fn (raw_cs, seris) => code raw_cs seris)); |
624 ) >> (fn (raw_cs, seris) => code raw_cs seris)); |
625 |
625 |
626 val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK]; |
626 val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK]; |
627 |
627 |
628 val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) = |
628 val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) = |
629 ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps"); |
629 ("export_code", "code_abstype", "code_axioms", "code_thms", "code_deps"); |
630 |
630 |
631 in |
631 in |
632 |
632 |
633 val codeP = |
633 val codeP = |
634 OuterSyntax.improper_command codeK "generate executable code for constants" |
634 OuterSyntax.improper_command codeK "generate executable code for constants" |