| changeset 35399 | 3881972fcfca |
| parent 33765 | 47b5db097646 |
| child 35413 | 4c7cba1f7ce9 |
--- a/src/Pure/Isar/specification.ML Sat Feb 27 13:55:03 2010 +0100 +++ b/src/Pure/Isar/specification.ML Sat Feb 27 20:51:51 2010 +0100 @@ -259,7 +259,7 @@ lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args); val notation = gen_notation (K I); -val notation_cmd = gen_notation ProofContext.read_const; +val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false); (* fact statements *)