globbing constant expressions use more idiomatic underscore rather than star

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 12:03:17 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 12:03:18 2010 +0100
@@ -1082,7 +1082,7 @@
     const: term
     ;
 
-    constexpr: ( const | 'name.*' | '*' )
+    constexpr: ( const | 'name._' | '_' )
     ;
 
     typeconstructor: nameref
@@ -1144,7 +1144,7 @@
     ;
 
     'code_reflect' string \\
-      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
+      ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
     ;
 

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 12:03:17 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 12:03:18 2010 +0100
@@ -1098,7 +1098,7 @@
     const: term
     ;
 
-    constexpr: ( const | 'name.*' | '*' )
+    constexpr: ( const | 'name._' | '_' )
     ;
 
     typeconstructor: nameref
@@ -1160,7 +1160,7 @@
     ;
 
     'code_reflect' string \\
-      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
+      ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
     ;
 

--- a/src/HOL/Codegenerator_Test/Generate.thy	Fri Nov 26 12:03:17 2010 +0100
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Nov 26 12:03:18 2010 +0100
@@ -14,6 +14,6 @@
   by a corresponding @{text export_code} command.
 *}
 
-export_code "*" checking SML OCaml? Haskell? Scala?
+export_code _ checking SML OCaml? Haskell? Scala?
 
 end

--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Nov 26 12:03:17 2010 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Nov 26 12:03:18 2010 +0100
@@ -19,6 +19,6 @@
   by a corresponding @{text export_code} command.
 *}
 
-export_code "*" checking SML OCaml? Haskell? Scala?
+export_code _ checking SML OCaml? Haskell? Scala?
 
 end

--- a/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:17 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:18 2010 +0100
@@ -349,7 +349,8 @@
 val _ = List.app Keyword.keyword [datatypesK, functionsK];
 
 val parse_datatype =
-  Parse.name --| Parse.$$$ "=" -- ((Parse.string >> (fn "*" => NONE | _ => Scan.fail ()))
+  Parse.name --| Parse.$$$ "=" --
+    (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
     || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
 
 in

--- a/src/Tools/Code/code_thingol.ML	Fri Nov 26 12:03:17 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Fri Nov 26 12:03:18 2010 +0100
@@ -940,9 +940,9 @@
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
-    fun read_const_expr "*" = ([], consts_of thy)
-      | read_const_expr s = if String.isSuffix ".*" s
-          then ([], consts_of_select (Context.this_theory thy (unsuffix ".*" s)))
+    fun read_const_expr "_" = ([], consts_of thy)
+      | read_const_expr s = if String.isSuffix "._" s
+          then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
           else ([Code.read_const thy s], []);
   in pairself flat o split_list o map read_const_expr end;