--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 11 13:15:14 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 11 13:15:14 2016 +0100
@@ -282,22 +282,22 @@
val IITN = "IITN"
val foldN = "fold"
val unfoldN = unN ^ foldN
-val uniqueN = "_unique"
-val transferN = "_transfer"
+val uniqueN = "unique"
+val transferN = "transfer"
val simpsN = "simps"
val ctorN = "ctor"
val dtorN = "dtor"
val ctor_foldN = ctorN ^ "_" ^ foldN
val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
-val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
+val ctor_fold_uniqueN = ctor_foldN ^ "_" ^ uniqueN
val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN
-val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
+val dtor_unfold_uniqueN = dtor_unfoldN ^ "_" ^ uniqueN
val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN
-val ctor_fold_transferN = ctor_foldN ^ transferN
-val dtor_unfold_transferN = dtor_unfoldN ^ transferN
+val ctor_fold_transferN = ctor_foldN ^ "_" ^ transferN
+val dtor_unfold_transferN = dtor_unfoldN ^ "_" ^ transferN
val ctor_mapN = ctorN ^ "_" ^ mapN
val dtor_mapN = dtorN ^ "_" ^ mapN
-val map_uniqueN = mapN ^ uniqueN
+val map_uniqueN = mapN ^ "_" ^ uniqueN
val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN
val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN
val min_algN = "min_alg"
@@ -323,12 +323,12 @@
val corecN = coN ^ recN
val ctor_recN = ctorN ^ "_" ^ recN
val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN
-val ctor_rec_transferN = ctor_recN ^ transferN
-val ctor_rec_uniqueN = ctor_recN ^ uniqueN
+val ctor_rec_transferN = ctor_recN ^ "_" ^ transferN
+val ctor_rec_uniqueN = ctor_recN ^ "_" ^ uniqueN
val dtor_corecN = dtorN ^ "_" ^ corecN
val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN
-val dtor_corec_transferN = dtor_corecN ^ transferN
-val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
+val dtor_corec_transferN = dtor_corecN ^ "_" ^ transferN
+val dtor_corec_uniqueN = dtor_corecN ^ "_" ^ uniqueN
val ctor_dtorN = ctorN ^ "_" ^ dtorN
val dtor_ctorN = dtorN ^ "_" ^ ctorN