# HG changeset patch
# User wenzelm
# Date 1166021253 -3600
# Node ID 7d4debbb1abf619a112bffa3803e35a6b0cd9f2a
# Parent  5a279c9138b6d7d8335447534c102c08a6f31927
edge: actually apply operation!

diff -r 5a279c9138b6 -r 7d4debbb1abf src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Wed Dec 13 15:47:31 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Wed Dec 13 15:47:33 2006 +0100
@@ -234,7 +234,7 @@
 
 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);
+  else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
 
 val begin_tag = edge #2 Latex.begin_tag;
 val end_tag = edge #1 Latex.end_tag;