src/Tools/Code/code_thingol.ML

     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 (ThyInfo.the_theory (unsuffix ".*" s) thy))
+          then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
           else ([Code.read_const thy s], []);
   in pairself flat o split_list o map read_const_expr end;
 
 fun code_depgr thy consts =
   let