# HG changeset patch
# User blanchet
# Date 1348646459 -7200
# Node ID 4339aa33535571717a616e0193c7c94de223cfc7
# Parent  7e856b6c5edcd41648e813d45e42e3951c9cc647
use singular since there is always only one theorem

diff -r 7e856b6c5edc -r 4339aa335355 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -96,9 +96,9 @@
   val unfoldsN: string
   val uniqueN: string
 
-  val mk_ctor_setsN: int -> string
+  val mk_ctor_setN: int -> string
+  val mk_dtor_setN: int -> string
   val mk_dtor_set_inductN: int -> string
-  val mk_dtor_setsN: int -> string
   val mk_exhaustN: string -> string
   val mk_injectN: string -> string
   val mk_nchotomyN: string -> string
@@ -207,8 +207,8 @@
 val rvN = "recover"
 val behN = "beh"
 fun mk_setsN i = mk_setN i ^ "s"
-val mk_ctor_setsN = prefix (ctorN ^ "_") o mk_setsN
-val mk_dtor_setsN = prefix (dtorN ^ "_") o mk_setsN
+val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN
+val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN
 fun mk_set_inductN i = mk_setN i ^ "_induct"
 val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN
 
diff -r 7e856b6c5edc -r 4339aa335355 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -2951,7 +2951,7 @@
              [(dtor_srelN, map single dtor_Jsrel_thms)]
            else
              []) @
-          map2 (fn i => fn thms => (mk_dtor_setsN i, map single thms)) ls' folded_set_simp_thmss
+          map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
diff -r 7e856b6c5edc -r 4339aa335355 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -1793,7 +1793,7 @@
              [(ctor_srelN, map single ctor_Isrel_thms)]
            else
              []) @
-          map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss
+          map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))