1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 12:03:17 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 12:03:18 2010 +0100
     1.3 @@ -1098,7 +1098,7 @@
     1.4      const: term
     1.5      ;
     1.6  
     1.7 -    constexpr: ( const | 'name.*' | '*' )
     1.8 +    constexpr: ( const | 'name._' | '_' )
     1.9      ;
    1.10  
    1.11      typeconstructor: nameref
    1.12 @@ -1160,7 +1160,7 @@
    1.13      ;
    1.14  
    1.15      'code_reflect' string \\
    1.16 -      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.17 +      ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.18        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    1.19      ;
    1.20