*** empty log message ***

1 files changed, 0 insertions, 12 deletions

diff --git a/hol-light/TacticRecording/graveyard.ml b/hol-light/TacticRecording/graveyard.ml
deleted file mode 100644
index db5c733d..00000000
--- a/hol-light/TacticRecording/graveyard.ml
+++ /dev/null
@@ -1,12 +0,0 @@
-
-
-(* Utility for applying tactic and incorproating results into goal tree.      *)
-(* Takes an "infotactic", i.e. like a normal tactic that works on 'goal' and  *)
-(* returns 'goalstate', but that also returns 'finfo' which summarises the    *)
-(* operation.  These are easily formed by tagging normal tactics.             *)
-
-let infotactic_wrap0 (infotac:goal->(goalstate*finfo)) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-  let ((meta,gs,just),gst) = infotac g in
-  let gxs = extend_gtree id gst gs in
-  (meta,gxs,just);;