# HG changeset patch
# User wenzelm
# Date 1254347063 -7200
# Node ID 2e4485b9a39f4eed835ddad3d1b211081298de75
# Parent  a0f38d8d633a8b9e7e1561f10a3aaaa72f684efe
eliminated dead code;

diff -r a0f38d8d633a -r 2e4485b9a39f src/Pure/Thy/html.ML
--- 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;
 
diff -r a0f38d8d633a -r 2e4485b9a39f src/Pure/envir.ML
--- 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;