--- a/src/Tools/Code/code_thingol.ML Wed Jul 21 15:23:46 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Jul 21 15:31:38 2010 +0200
@@ -910,7 +910,7 @@
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 (Thy_Info.the_theory (unsuffix ".*" s) thy))
+ 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;