| changeset 55954 | a29aefc88c8d |
| parent 55765 | ec7ca5388dea |
| child 55955 | e8f1bf005661 |
--- a/src/Pure/Isar/proof.ML Thu Mar 06 12:58:51 2014 +0100 +++ b/src/Pure/Isar/proof.ML Thu Mar 06 13:44:01 2014 +0100 @@ -581,7 +581,7 @@ val write_cmd = gen_write (fn ctxt => fn (c, mx) => - (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx)); + (Proof_Context.read_const ctxt {proper = false, strict = false} (Mixfix.mixfixT mx) c, mx)); end;