edge: actually apply operation!

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