1 files changed, 0 insertions, 13 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 470c85674..07d4049ce 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -186,16 +186,3 @@ let init () =
   add_frozen_state ();
   path_prefix := []
 
-
-(* Rollback. *)
-
-let with_heavy_rollback f x =
-  let sum = freeze_summaries ()
-  and flib = freeze() in
-  try 
-    f x
-  with reraise -> begin
-    unfreeze_summaries sum;
-    unfreeze flib;
-    raise reraise
-  end