# HG changeset patch
# User blanchet
# Date 1346831917 -7200
# Node ID aca966dc18f6e889fffe5ee88b79e6a49fc1c506
# Parent  cb80b6404f8eddb70559c044d8ccc69c982f2009
added comment for Dmitriy

diff -r cb80b6404f8e -r aca966dc18f6 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 09:54:20 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 09:58:37 2012 +0200
@@ -254,6 +254,8 @@
 fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
   [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
 
+(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
+   also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
 fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
   (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;