diff -r c32b64394963 -r 274426d1adbc src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Mar 15 18:22:39 2000 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Mar 15 18:24:27 2000 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Simple LaTeX presentation primitives (based on outer lexical syntax).
+LaTeX presentation primitives (based on outer lexical syntax).
 *)
 
 signature LATEX =
@@ -88,12 +88,21 @@
 
 (* theory presentation *)
 
-val isabelle_simple = enclose "\\begin{isabellesimple}%\n" "\\end{isabellesimple}%\n";
+val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n";
 
-val old_symbol_source = isabelle_simple o output_symbols;
-val token_source = isabelle_simple o output_tokens;
+val old_symbol_source = isabelle_env o output_symbols;
+val token_source = isabelle_env o output_tokens;
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
 
 
+(* print mode *)
+
+fun latex_output str =
+  let val syms = Symbol.explode str
+  in (output_symbols syms, real (Symbol.length syms)) end;
+
+val _ = Symbol.add_mode "latex" latex_output;
+
+
 end;