--- 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
@@ -36,6 +36,8 @@
val ctor_recN: string
val ctor_recsN: string
val ctor_relN: string
+ val ctor_set_inclN: string
+ val ctor_set_set_inclN: string
val ctor_srelN: string
val disc_unfold_iffN: string
val disc_unfoldsN: string
@@ -51,6 +53,8 @@
val dtor_exhaustN: string
val dtor_injectN: string
val dtor_map_uniqueN: string
+ val dtor_set_inclN: string
+ val dtor_set_set_inclN: string
val dtor_srelN: string
val dtor_strong_coinductN: string
val dtor_unfoldN: string
@@ -249,7 +253,11 @@
val hsetN = "Hset"
val hset_recN = hsetN ^ "_rec"
val set_inclN = "set_incl"
+val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
+val dtor_set_inclN = dtorN ^ "_" ^ set_inclN
val set_set_inclN = "set_set_incl"
+val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN
+val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN
val caseN = "case"
val discN = "disc"