| changeset 22207 | 4bc4a930a8bc |
| parent 21858 | 05f57309170c |
| child 22227 | 7f88a6848fc2 |
--- a/src/Pure/General/xml.ML Tue Jan 30 08:21:13 2007 +0100 +++ b/src/Pure/General/xml.ML Tue Jan 30 08:21:15 2007 +0100 @@ -28,7 +28,7 @@ val parse_elem: string list -> tree * string list val parse_document: string list -> (string option * tree) * string list val tree_of_string: string -> tree - (* scanner for stream parser in proof_general.ML *) + (* scanner for stream parser in proof_general.ML *) val scan_comment_whspc : string list -> unit * string list end;