src/Pure/ML/ml_profiling.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_profiling.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,19 @@
+(*  Title:      Pure/ML/ml_profiling.ML
+    Author:     Makarius
+
+Profiling for Poly/ML 5.6.
+*)
+
+structure ML_Profiling =
+struct
+
+fun profile_time pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+
+fun profile_time_thread pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+
+fun profile_allocations pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+
+end;