--- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -1734,8 +1734,8 @@
val Isrel_defs = map srel_def_of_bnf Ibnfs;
val Irel_defs = map rel_def_of_bnf Ibnfs;
- val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
- val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
+ val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
+ val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
val folded_ctor_map_thms = map fold_maps ctor_map_thms;
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
@@ -1749,13 +1749,14 @@
in
map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
- fn set_naturals => fn set_incls => fn set_set_inclss =>
+ fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
(K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
- ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
+ ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
- ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
+ ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
+ ctor_set_set_incl_thmsss
end;
val ctor_Irel_thms =
@@ -1784,8 +1785,8 @@
[(ctor_mapN, map single folded_ctor_map_thms),
(ctor_relN, map single ctor_Irel_thms),
(ctor_srelN, map single ctor_Isrel_thms),
- (set_inclN, set_incl_thmss),
- (set_set_inclN, map flat set_set_incl_thmsss)] @
+ (ctor_set_inclN, ctor_set_incl_thmss),
+ (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>