| changeset 55955 | e8f1bf005661 |
| parent 55954 | a29aefc88c8d |
| child 55997 | 9dc5ce83202c |
--- a/src/Pure/Isar/specification.ML Thu Mar 06 13:44:01 2014 +0100 +++ b/src/Pure/Isar/specification.ML Thu Mar 06 14:38:54 2014 +0100 @@ -281,7 +281,7 @@ val notation = gen_notation (K I); val notation_cmd = - gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false} dummyT); + gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false}); end;