| changeset 43485 | 33a24212a72d |
| parent 42290 | b1f544c84040 |
| child 43709 | 717e96cf9527 |
--- a/src/Pure/Thy/latex.ML Mon Jun 20 23:19:38 2011 +0200 +++ b/src/Pure/Thy/latex.ML Mon Jun 20 23:21:24 2011 +0200 @@ -102,7 +102,8 @@ if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s else output_chrs sym | Symbol.Raw s => s - | Symbol.Malformed s => error (Symbol.malformed_msg s)); + | Symbol.Malformed s => error (Symbol.malformed_msg s) + | Symbol.EOF => error "Bad EOF symbol"); in