Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped comment after conversation with author: predicate compiler works independently from any code generator setup
authorhaftmann
Sat, 17 Dec 2016 15:22:00 +0100
changeset 64583 2edac4e13918
parent 64582 3d20ded18f14
child 64584 142ac30b68fe
dropped comment after conversation with author: predicate compiler works independently from any code generator setup
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle