--- 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*)