src/HOL/BNF/Tools/bnf_fp.ML
changeset 49543 53b3c532a082
parent 49542 b39354db8629
child 49544 24094fa47e0d
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -32,6 +32,7 @@
   val ctor_fold_uniqueN: string
   val ctor_foldsN: string
   val ctor_mapN: string
+  val ctor_map_uniqueN: string
   val ctor_recN: string
   val ctor_recsN: string
   val ctor_relN: string
@@ -49,6 +50,7 @@
   val dtor_ctorN: string
   val dtor_exhaustN: string
   val dtor_injectN: string
+  val dtor_map_uniqueN: string
   val dtor_srelN: string
   val dtor_strong_coinductN: string
   val dtor_unfoldN: string
@@ -186,6 +188,8 @@
 val ctor_mapN = ctorN ^ "_" ^ mapN
 val dtor_mapN = dtorN ^ "_" ^ mapN
 val map_uniqueN = mapN ^ uniqueN
+val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN
+val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN
 val min_algN = "min_alg"
 val morN = "mor"
 val bisN = "bis"