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