# HG changeset patch
# User berghofe
# Date 1217977107 -7200
# Node ID c1e60d8cba07387e04668618315c7b1f0ad1bd88
# Parent  650af1991b8bfc518f83321875f7b567e841e86d
Reverted last change, since it caused incompatibilities.

diff -r 650af1991b8b -r c1e60d8cba07 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Aug 06 00:12:31 2008 +0200
+++ b/src/Pure/codegen.ML	Wed Aug 06 00:58:27 2008 +0200
@@ -681,8 +681,7 @@
                  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,
-                   map (preprocess_term thy) (quotes_of ms));
+                 val (gr3, ps3) = codegens false (gr2, 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