--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 22:56:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 23:01:04 2013 +0200
@@ -604,7 +604,7 @@
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
val nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
- val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
+ val nested_set_maps = maps set_map_of_bnf nested_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -687,7 +687,7 @@
val thm =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_map's
+ mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_maps
pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -1170,8 +1170,8 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs;
- val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
+ val nesting_set_maps = maps set_map_of_bnf nesting_bnfs;
+ val nested_set_maps = maps set_map_of_bnf nested_bnfs;
val live = live_of_bnf any_fp_bnf;
val _ =
@@ -1330,7 +1330,7 @@
fun mk_set_thm fp_set_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
- (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
+ (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @
(if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set)
(cterm_instantiate_pos [SOME cxIn] fp_set_thm))
|> singleton (Proof_Context.export names_lthy no_defs_lthy);