src/Tools/Code/code_thingol.ML
changeset 40711 81bc73585eec
parent 39566 87a5704673f0
child 40726 16dcfedc4eb7
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Nov 26 12:03:17 2010 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Nov 26 12:03:18 2010 +0100
     1.3 @@ -940,9 +940,9 @@
     1.4      fun belongs_here thy' c = forall
     1.5        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     1.6      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     1.7 -    fun read_const_expr "*" = ([], consts_of thy)
     1.8 -      | read_const_expr s = if String.isSuffix ".*" s
     1.9 -          then ([], consts_of_select (Context.this_theory thy (unsuffix ".*" s)))
    1.10 +    fun read_const_expr "_" = ([], consts_of thy)
    1.11 +      | read_const_expr s = if String.isSuffix "._" s
    1.12 +          then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
    1.13            else ([Code.read_const thy s], []);
    1.14    in pairself flat o split_list o map read_const_expr end;
    1.15