# HG changeset patch
# User wenzelm
# Date 1165786025 -3600
# Node ID c7ca3b57557fd48d1ed651dbf091fc1cf14fab5e
# Parent  d4fd9bb0ccd63c96b33adbfd1f54460eeaa8ab2a
tuned;

diff -r d4fd9bb0ccd6 -r c7ca3b57557f src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Sun Dec 10 22:27:03 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Sun Dec 10 22:27:05 2006 +0100
@@ -232,13 +232,14 @@
 fun err_bad_nesting pos =
   error ("Bad nesting of commands in presentation" ^ pos);
 
-fun edge1 f (x : string option, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else x));
-fun edge2 f (x : string option, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else y));
+fun edge which f (x: string option, y) =
+  if x = y then I
+  else (case which (x, y) of NONE => I | SOME txt => Buffer.add txt);
 
-val begin_tag = edge2 Latex.begin_tag;
-val end_tag = edge1 Latex.end_tag;
-fun open_delim delim e = edge2 Latex.begin_delim e #> delim #> edge2 Latex.end_delim e;
-fun close_delim delim e = edge1 Latex.begin_delim e #> delim #> edge1 Latex.end_delim e;
+val begin_tag = edge #2 Latex.begin_tag;
+val end_tag = edge #1 Latex.end_tag;
+fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
+fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
 
 in