doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 40709 b29c70cd5c93
parent 40388 cb9fd7dd641c
child 40711 81bc73585eec
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 11:06:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 11:38:20 2010 +0100
@@ -1143,7 +1143,8 @@
     'code_modulename' target ( ( string string ) + )
     ;
 
-    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+    'code_reflect' string \\
+      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
     ;