--- a/src/Pure/Isar/outer_syntax.ML Wed Jul 03 15:19:36 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 03 16:19:57 2013 +0200
@@ -34,7 +34,6 @@
val parse: Position.T -> string -> Toplevel.transition list
type isar
val isar: TextIO.instream -> bool -> isar
- val span_cmts: Token.T list -> Token.T list
val read_span: outer_syntax -> Token.T list -> Toplevel.transition
end;
@@ -277,22 +276,6 @@
|> toplevel_source term (SOME true) lookup_commands_dynamic;
-(* side-comments *)
-
-local
-
-fun cmts (t1 :: t2 :: toks) =
- if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
- else cmts (t2 :: toks)
- | cmts _ = [];
-
-in
-
-val span_cmts = filter Token.is_proper #> cmts;
-
-end;
-
-
(* read command span -- fail-safe *)
fun read_span outer_syntax toks =