changeset 60924 | 610794dff23c |
parent 60693 | 044f8bb3dd30 |
child 61579 | 634cd44bb1d3 |
--- a/src/Pure/Isar/outer_syntax.ML Wed Aug 12 21:38:39 2015 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Thu Aug 13 11:05:19 2015 +0200 @@ -86,7 +86,7 @@ ); val get_commands = Data.get; -val dest_commands = get_commands #> Symtab.dest #> sort_wrt #1; +val dest_commands = get_commands #> Symtab.dest #> sort_by #1; val lookup_commands = Symtab.lookup o get_commands; fun help thy pats =