changeset 55954 | a29aefc88c8d |
parent 55765 | ec7ca5388dea |
child 55955 | e8f1bf005661 |
55953:b19373bd7ea8 | 55954:a29aefc88c8d |
---|---|
579 |
579 |
580 val write = gen_write (K I); |
580 val write = gen_write (K I); |
581 |
581 |
582 val write_cmd = |
582 val write_cmd = |
583 gen_write (fn ctxt => fn (c, mx) => |
583 gen_write (fn ctxt => fn (c, mx) => |
584 (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx)); |
584 (Proof_Context.read_const ctxt {proper = false, strict = false} (Mixfix.mixfixT mx) c, mx)); |
585 |
585 |
586 end; |
586 end; |
587 |
587 |
588 |
588 |
589 (* fix *) |
589 (* fix *) |