1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:06:49 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:38:20 2010 +0100
     1.3 @@ -1159,7 +1159,8 @@
     1.4      'code_modulename' target ( ( string string ) + )
     1.5      ;
     1.6  
     1.7 -    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
     1.8 +    'code_reflect' string \\
     1.9 +      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.10        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    1.11      ;
    1.12