src/Pure/codegen.ML
changeset 27758 c1e60d8cba07
parent 27724 0cc30a837f26
child 28054 2b84d34c5d02
     1.1 --- a/src/Pure/codegen.ML	Wed Aug 06 00:12:31 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Wed Aug 06 00:58:27 2008 +0200
     1.3 @@ -681,8 +681,7 @@
     1.4                   val (ts1, ts2) = args_of ms ts;
     1.5                   val (gr1, ps1) = codegens false (gr, ts1);
     1.6                   val (gr2, ps2) = codegens true (gr1, ts2);
     1.7 -                 val (gr3, ps3) = codegens false (gr2,
     1.8 -                   map (preprocess_term thy) (quotes_of ms));
     1.9 +                 val (gr3, ps3) = codegens false (gr2, quotes_of ms);
    1.10                   val (gr4, _) = invoke_tycodegen thy defs dep module false
    1.11                     (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
    1.12                   val (module', suffix) = (case get_defn thy defs s T of