--- 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
--- 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, [])]))
--- 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, [])]))