Linker error: using pulseIn() realized as puls_asm.S

Using the pulseIn() method in a sketch (e.g.)

#define PULSE_PIN 3
void setup() {
  Serial.begin(115200);
  pinMode(PULSE_PIN, INPUT_PULLUP);
  uint32_t pulse = pulseIn(PULSE_PIN, HIGH, 6000);
  Serial.print  ("pulse len[us]: ");
  Serial.println(pulse);  
}
void loop() {}

does create an linker error: see output log:

c:/users/.../appdata/local/arduino15/packages/sandeepmistry/tools/gcc-arm-none-eabi/5_2-2015q4/bin/../lib/gcc/arm-none-eabi/5.2.1/../../../../arm-none-eabi/bin/ld.exe: 
error: C:\Users\...\AppData\Local\Temp\build564232db8aa323b9aba1a2502c4097a0.tmp/test_pulseIn.ino.elf 
uses VFP register arguments, 
C:\Users\...\AppData\Local\Temp\build564232db8aa323b9aba1a2502c4097a0.tmp/core\core.a(pulse_asm.S.o) 
does not

c:/users/.../appdata/local/arduino15/packages/sandeepmistry/tools/gcc-arm-none-eabi/5_2-2015q4/bin/../lib/gcc/arm-none-eabi/5.2.1/../../../../arm-none-eabi/bin/ld.exe: 
failed to merge target specific data of file C:\Users\...\AppData\Local\Temp\build564232db8aa323b9aba1a2502c4097a0.tmp/core\core.a(pulse_asm.S.o)

In the assumption that the DUE configuration (platform.txt) has a proper setting, I have tried to find a difference but I'm not succesful up to now.