# HG changeset patch
# User haftmann
# Date 1249030149 -7200
# Node ID 3f7984175fdd4d0f362b47216c78033eecd0ef7c
# Parent  36dbff4841ab9360972b36ca58e7abbe90bf1dc4
added a somehow clueless comment

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