Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 53285 f09645642984
parent 53270 c8628119d18e
child 53290 b6c3be868217 
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 20:15:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -602,8 +602,8 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
-    val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_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 fp_b_names = map base_name_of_typ fpTs;
@@ -726,7 +726,7 @@
         val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
 
         val tacss =
-          map2 (map o mk_iter_tac pre_map_defs (nested_map_ids'' @ nesting_map_ids'') iter_defs)
+          map2 (map o mk_iter_tac pre_map_defs (nested_map_id's @ nesting_map_id's) iter_defs)
             ctor_iter_thms ctr_defss;
 
         fun prove goal tac =
@@ -763,7 +763,7 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+    val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
     val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;
@@ -919,10 +919,10 @@
         val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
 
         val unfold_tacss =
-          map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
+          map3 (map oo mk_coiter_tac unfold_defs nesting_map_id's)
             (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
         val corec_tacss =
-          map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'')
+          map3 (map oo mk_coiter_tac corec_defs nesting_map_id's)
             (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
 
         fun prove goal tac =
isabelle