src/Tools/Code/code_thingol.ML
changeset 37216 3165bc303f66
parent 36960 01594f816e3a
child 37384 5aba26803073
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -882,7 +882,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 (ThyInfo.the_theory (unsuffix ".*" s) thy))
     1.8 +          then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
     1.9            else ([Code.read_const thy s], []);
    1.10    in pairself flat o split_list o map read_const_expr end;
    1.11