equal
deleted
inserted
replaced
587 >> (Thm.declaration_attribute o K)) "tracing of the code generator preprocessor" |
587 >> (Thm.declaration_attribute o K)) "tracing of the code generator preprocessor" |
588 end); |
588 end); |
589 |
589 |
590 val _ = |
590 val _ = |
591 Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup" |
591 Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup" |
592 (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of))); |
592 (Scan.succeed (Toplevel.keep (print_codeproc o Toplevel.context_of))); |
593 |
593 |
594 end; (*struct*) |
594 end; (*struct*) |