1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 21 15:23:46 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 21 15:31:38 2010 +0200
     1.3 @@ -910,7 +910,7 @@
     1.4      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     1.5      fun read_const_expr "*" = ([], consts_of thy)
     1.6        | read_const_expr s = if String.isSuffix ".*" s
     1.7 -          then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
     1.8 +          then ([], consts_of_select (Context.this_theory thy (unsuffix ".*" s)))
     1.9            else ([Code.read_const thy s], []);
    1.10    in pairself flat o split_list o map read_const_expr end;
    1.11