diff -r 36dbff4841ab -r 3f7984175fdd src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Jul 31 10:49:08 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Jul 31 10:49:09 2009 +0200
@@ -109,7 +109,10 @@
   | apply_functrans thy c [] eqns = eqns
   | apply_functrans thy c functrans eqns = eqns
       |> perhaps (perhaps_loop (perhaps_apply functrans))
-      |> Code.assert_eqns_const thy c;
+      |> Code.assert_eqns_const thy c
+      (*FIXME in future, the check here should be more accurate wrt. type schemes
+      -- perhaps by means of upcoming code certificates with a corresponding
+         preprocessor protocol*);
 
 fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);