# 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;