I've found the problem: The bit WGM12 is actually in TCCR1B, not TCCR1A. The code below is working, generating a 8 MHz clock on pin 9 (Arduino Micro). Thanks to everybody for the help!
//
//
// Use of timer1 to generate 8 Mhz clock on pin 9
//
//
const int freqOutputPin = 9; // OC1A output pin for ATmega32u4 (Arduino Micro)
// Constants are computed at compile time
// If you change the prescale value, it affects CS22, CS21, and CS20
// For a given prescale value, the eight-bit number that you
// load into OCR1A determines the frequency according to the
// following formulas:
//
// With no prescaling, an ocr1val of 0 causes the output pin to
// toggle the value every CPU clock cycle. That is, the
// period is equal to two clock cycles.
//
// With F_CPU = 16 MHz, the result is 8 MHz.
//
// To change the timer prescale division, use different bits for CS22:0 below
const int ocr1aval = 0;
void setup()
{
pinMode(freqOutputPin, OUTPUT);
// Set Timer 1 CTC mode with no prescaling. OC1A toggles on compare match
//
// WGM12:0 = 010: CTC Mode, toggle OC
// WGM2 bits 1 and 0 are in TCCR1A,
// WGM2 bit 2 and 3 are in TCCR1B
// COM1A0 sets OC1A (arduino pin 9 on Arduino Micro) to toggle on compare match
//
TCCR1A = ( (1 << COM1A0));
// Set Timer 1 No prescaling (i.e. prescale division = 1)
//
TCCR1B = ((1 << WGM12) | (1 << CS10));
// Make sure Compare-match register A interrupt for timer1 is disabled
TIMSK1 = 0;
// This value determines the output frequency
OCR1A = ocr1aval;
}
void loop()
{
//
}