# HG changeset patch
# User bulwahn
# Date 1243533698 -7200
# Node ID 4e87577544aeb10fce1cfffbdafc740a522d5422
# Parent  86093a969bcd2bf22ff5e072e742908bfc1b04d3
added remark to code

diff -r 86093a969bcd -r 4e87577544ae 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