added remark to code
authorbulwahn
Thu, 28 May 2009 20:01:38 +0200
changeset 31284 4e87577544ae
parent 31283 86093a969bcd
child 31286 424874813840
added remark to code
src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Thu May 28 18:59:51 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Thu May 28 20:01:38 2009 +0200
@@ -965,6 +965,7 @@
   | select_sup _ 1 = [rtac @{thm supI1}]
   | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
 
+(* FIXME: This function relies on the derivation of an induction rule *)
 fun get_nparams thy s = let
     val _ = tracing ("get_nparams: " ^ s)
   in