diff -r 17d30843fc3b -r e8d2ecf6aaac src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Mon Feb 25 11:07:02 2013 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Mon Feb 25 12:17:11 2013 +0100 @@ -293,7 +293,7 @@ end; -(* read toplevel commands -- fail-safe *) +(* read command span -- fail-safe *) fun read_span outer_syntax toks = let