author | wenzelm |
Mon, 19 Mar 2012 18:18:42 +0100 | |
changeset 47014 | e203b7d7e08d |
parent 47013 | 95bd95addb24 |
child 47020 | 63e23fc6259b |
--- a/src/Pure/Isar/outer_syntax.ML Mon Mar 19 15:56:27 2012 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Mon Mar 19 18:18:42 2012 +0100 @@ -130,7 +130,7 @@ val _ = (case try (Thy_Header.the_keyword thy) name of SOME spec => - if Option.map Keyword.spec spec = SOME kind then () + if Option.map #1 spec = SOME (Keyword.kind_of kind) then () else error ("Inconsistent outer syntax keyword declaration " ^ quote name) | NONE => if Context.theory_name thy = Context.PureN