# HG changeset patch
# User haftmann
# Date 1285329824 -7200
# Node ID d36864e3f06c4881ec2b4204a4a34f9f91cc54b2
# Parent  d9fb92a8c80a2cd829f9fdfae08a01ddf67936e0
dropped dead code

diff -r d9fb92a8c80a -r d36864e3f06c src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Sep 24 14:03:44 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Sep 24 14:03:44 2010 +0200
@@ -480,7 +480,6 @@
       present_code thy (mk_cs thy)
         (fn naming => maps (fn f => f thy naming) mk_stmtss)
         target some_width "Example" []
-      (*|> Latex.output_typewriter*)
     end);
 
 end;