# HG changeset patch
# User haftmann
# Date 1290767900 -3600
# Node ID b29c70cd5c93b138488b5581d62471b1ce26561f
# Parent  739dc2c2ba24a25ca5279070513deb4842a28b7d
datatype constructor glob for code_reflect

diff -r 739dc2c2ba24 -r b29c70cd5c93 doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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 ) ?
     ;
 
diff -r 739dc2c2ba24 -r b29c70cd5c93 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:06:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 11:38:20 2010 +0100
@@ -1159,7 +1159,8 @@
     'code_modulename' target ( ( string string ) + )
     ;
 
-    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+    'code_reflect' string \\
+      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
     ;