1 files changed, 12 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/graveyard.ml b/hol-light/TacticRecording/graveyard.ml
new file mode 100644
index 00000000..db5c733d
--- /dev/null
+++ b/hol-light/TacticRecording/graveyard.ml
@@ -0,0 +1,12 @@
+
+
+(* 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);;