eliminated dead code;

--- a/src/Pure/Thy/html.ML	Wed Sep 30 23:30:37 2009 +0200
+++ b/src/Pure/Thy/html.ML	Wed Sep 30 23:44:23 2009 +0200
@@ -222,7 +222,6 @@
     in (implode syms, width) end;
 
 val output = #1 o output_width;
-val output_symbols = map #2 o output_syms;
 
 val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
 

--- a/src/Pure/envir.ML	Wed Sep 30 23:30:37 2009 +0200
+++ b/src/Pure/envir.ML	Wed Sep 30 23:44:23 2009 +0200
@@ -62,8 +62,8 @@
   tenv: tenv,           (*assignments to Vars*)
   tyenv: Type.tyenv};   (*assignments to TVars*)
 
-fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
-fun map_env f (Envir {maxidx, tenv, tyenv}) = make_env (f (maxidx, tenv, tyenv));
+fun make_env (maxidx, tenv, tyenv) =
+  Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
 
 fun maxidx_of (Envir {maxidx, ...}) = maxidx;
 fun term_env (Envir {tenv, ...}) = tenv;