equal
deleted
inserted
replaced
114 |
114 |
115 val typecheck_meth = |
115 val typecheck_meth = |
116 Method.only_sectioned_args |
116 Method.only_sectioned_args |
117 [Args.add -- Args.colon >> K (I, TC_add), |
117 [Args.add -- Args.colon >> K (I, TC_add), |
118 Args.del -- Args.colon >> K (I, TC_del)] |
118 Args.del -- Args.colon >> K (I, TC_del)] |
119 (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))); |
119 (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))); |
120 |
120 |
121 val _ = |
121 val _ = |
122 OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag |
122 OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag |
123 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
123 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
124 Toplevel.keep (print_tcset o Toplevel.context_of))); |
124 Toplevel.keep (print_tcset o Toplevel.context_of))); |