# HG changeset patch
# User haftmann
# Date 1481984520 -3600
# Node ID 2edac4e139181ed800bae63fe562418525dbca0c
# Parent  3d20ded18f14e5c8549083cb563f12e039ca85b3
dropped comment after conversation with author: predicate compiler works independently from any code generator setup

diff -r 3d20ded18f14 -r 2edac4e13918 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Dec 17 14:47:41 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sat Dec 17 15:22:00 2016 +0100
@@ -141,8 +141,6 @@
       | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
       | flatten' (t as _ $ _) (names, prems) =
       if is_constrt ctxt t orelse keep_functions thy t then
-       (* FIXME: constructor terms are supposed to be seen in the way the code generator
-          sees constructors?*)
         [(t, (names, prems))]
       else
         case (fst (strip_comb t)) of