src/HOL/Codatatype/Tools/bnf_def.ML

 
 
 
 (* Names *)
 
-fun nonzero_string_of_int 0 = ""
-  | nonzero_string_of_int n = string_of_int n;
-
 val mapN = "map";
 val setN = "set";
 fun mk_setN i = setN ^ nonzero_string_of_int i;
 val bdN = "bd";
 val witN = "wit";

   let
     val fact_policy = mk_fact_policy no_defs_lthy;
     val b = qualify raw_b;
     val live = length raw_sets;
     val nwits = length raw_wits;
+
+    val _ = tracing (Binding.name_of b)
 
     val map_rhs = prep_term no_defs_lthy raw_map;
     val set_rhss = map (prep_term no_defs_lthy) raw_sets;
     val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of
       Abs (_, T, t) => (T, t)