code simplification

[helm.git] / matita / matita / matitaGui.ml

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index d8916f7fa923e21cf11b9b25644f9628a171a360..71e7c2c00ebe275dafc20145b0845e8284833a9a 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -589,7 +589,7 @@ class gui () =
                match !id with
                | None -> assert false (* a race condition occurred *)
                | Some id ->
-                   (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id));
+                   source_view#source_buffer#misc#disconnect id));
              source_view#source_buffer#place_cursor
               (source_view#source_buffer#get_iter (`OFFSET x'));
         end;