Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014

[digitig <digitig@gmail.com>]

In main.ads I have:

package Main
with SPARK_Mode => On
is
   procedure Test;
end Main;

In main.adb I have:

with Ada.Numerics.Discrete_Random;
with Ada.Text_IO;
package body Main
with SPARK_Mode => On
is
   procedure Test is
      subtype Die is Integer range 1 .. 6;
      subtype Dice is Integer range 2*Die'First .. 2*Die'Last;
      package Random_Die is new Ada.Numerics.Discrete_Random (Die);
      use Random_Die;
      G : Generator;
      D : Dice;
   begin
      Reset (G);  -- Start the generator in a unique state in each run
      loop
         -- Roll a pair of dice; sum and process the results
         D := Random(G) + Random(G);
         Ada.Text_IO.Put_Line(D'Image);
      end loop;
   end Test;
end Main;

Running SPARK | Examine all sources from GPS gives me the error:

        9:7 "Random_Die" is not a library-level package
        9:7 incorrect placement of aspect "Spark_Mode"
        9:7 instantiation error at a-nudira.ads:45

Line 9 is:

      package Random_Die is new Ada.Numerics.Discrete_Random (Die);

But the error points into a line in the GNAT library, in a-nudira.ads that simply says

        SPARK_Mode => Off

I'm completely bewildered here - what's wrong with my code here (other than it being a toy example)? And how *do* I use Ada.Numerics.Discrete_Random in conjunction with SPARK?