# HG changeset patch
# User blanchet
# Date 1376256959 -7200
# Node ID bb8787b20437075b356f406fd99e07bceb2a873c
# Parent  f583d7b72d4e9ae5a8e9883595d0d34924977b1c
added warning

diff -r f583d7b72d4e -r bb8787b20437 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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)