--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Sun Aug 11 23:35:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Sun Aug 11 23:35:59 2013 +0200
@@ -1099,6 +1099,11 @@
val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
val live = live_of_bnf any_fp_bnf;
+ val _ =
+ if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then
+ warning ("Map function and relator names ignored")
+ else
+ ();
val Bs =
map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)