diff -r a5ffe85460af -r cedf9610b71d src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Tue Jul 10 09:23:16 2007 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Tue Jul 10 09:23:17 2007 +0200
@@ -18,7 +18,7 @@
   val read_bare_const: theory -> string -> string * typ
   val read_const: theory -> string -> const
   val read_const_exprs: theory -> (const list -> const list)
-    -> string list -> const list
+    -> string list -> bool * const list
 
   val co_of_const: theory -> const
     -> string * ((string * sort) list * (string * typ list))
@@ -120,8 +120,10 @@
 
 in
 
-fun read_const_exprs thy select =
-  (op @) o apsnd select o pairself flat o split_list o map (read_const_expr thy);
+fun read_const_exprs thy select exprs =
+  case (pairself flat o split_list o map (read_const_expr thy)) exprs
+   of (consts, []) => (false, consts)
+    | (consts, consts') => (true, consts @ select consts');
 
 end; (*local*)