src/Pure/Tools/build.ML

         (Thy_Info.use_theories {
           document = Present.document_enabled (Options.string options "document"),
           symbols = symbols,
           last_timing = last_timing,
           master_dir = master_dir}
+        |>
+          (case Options.string options "profiling" of
+            "" => I
+          | "time" => profile_time
+          | "allocations" => profile_allocations
+          | bad => error ("Bad profiling option: " ^ quote bad))
         |> Unsynchronized.setmp print_mode
             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
     else
       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
         " (undefined " ^ commas conds ^ ")\n")