# HG changeset patch
# User blanchet
# Date 1452514514 -3600
# Node ID 438f5986d11c3ef26165ffbc4a2a425101cb7066
# Parent  d0dff7a80c267bc1663822bd39ca5f69e70f9336
tuning

diff -r d0dff7a80c26 -r 438f5986d11c src/HOL/Tools/BNF/bnf_fp_util.ML
--- 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