| changeset 42287 | d98eb048a2e4 |
| parent 42042 | 264f8d0e899f |
| child 42360 | da8817d01e7c |
--- a/src/Pure/Isar/proof.ML Fri Apr 08 14:05:31 2011 +0200 +++ b/src/Pure/Isar/proof.ML Fri Apr 08 14:20:57 2011 +0200 @@ -566,7 +566,7 @@ val write_cmd = gen_write (fn ctxt => fn (c, mx) => - (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx)); + (ProofContext.read_const ctxt false (Mixfix.mixfixT mx) c, mx)); end;