# HG changeset patch # User berghofe # Date 1217869055 -7200 # Node ID 0cc30a837f26baf48eae1363bfed1bb7411ce333 # Parent ce8f79b91ed117a3467c0ffa50ca05c1667cfe31 Quoted terms in consts_code declarations are now preprocessed as well. diff -r ce8f79b91ed1 -r 0cc30a837f26 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Mon Aug 04 18:56:55 2008 +0200 +++ b/src/Pure/codegen.ML Mon Aug 04 18:57:35 2008 +0200 @@ -681,7 +681,8 @@ val (ts1, ts2) = args_of ms ts; val (gr1, ps1) = codegens false (gr, ts1); val (gr2, ps2) = codegens true (gr1, ts2); - val (gr3, ps3) = codegens false (gr2, quotes_of ms); + val (gr3, ps3) = codegens false (gr2, + map (preprocess_term thy) (quotes_of ms)); val (gr4, _) = invoke_tycodegen thy defs dep module false (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T); val (module', suffix) = (case get_defn thy defs s T of