diff -r 751bcf0473a7 -r 3498c66b5e55 src/Pure/ML/ml_profiling.ML
--- a/src/Pure/ML/ml_profiling.ML	Sat Apr 02 22:38:26 2016 +0200
+++ b/src/Pure/ML/ml_profiling.ML	Sat Apr 02 22:46:12 2016 +0200
@@ -4,7 +4,14 @@
 Profiling for Poly/ML 5.6.
 *)
 
-structure ML_Profiling =
+signature ML_PROFILING =
+sig
+  val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
+  val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
+  val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
+end;
+
+structure ML_Profiling: ML_PROFILING =
 struct
 
 fun profile_time pr f x =