doc-src/IsarRef/Thy/Inner_Syntax.thy
changeset 39348 600de0485859
parent 39285 af73cf0dc31f
child 39376 12dac4b58df8
     1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Sep 03 10:58:11 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Sep 03 11:21:58 2010 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4    \begin{mldecls} 
     1.5      @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
     1.6      @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
     1.7 -    @{index_ML show_consts: "bool Unsynchronized.ref"} & default @{ML false} \\
     1.8 +    @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     1.9      @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
    1.10      @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
    1.11      @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\