# HG changeset patch
# User blanchet
# Date 1377865039 -7200
# Node ID c31c0c311cf080ad0710a7a1bc9d988944fa8dbc
# Parent  9228c575d67db5d971ce3ac1b38f58bf5eee07e5
more canonical naming

diff -r 9228c575d67d -r c31c0c311cf0 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 30 14:17:19 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_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 nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+    val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_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;
@@ -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_id's @ nesting_map_id's) iter_defs)
+          map2 (map o mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) 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_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+    val nesting_map_idents = 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_id's)
+          map3 (map oo mk_coiter_tac unfold_defs nesting_map_idents)
             (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_id's)
+          map3 (map oo mk_coiter_tac corec_defs nesting_map_idents)
             (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
 
         fun prove goal tac =
diff -r 9228c575d67d -r c31c0c311cf0 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Aug 30 14:17:19 2013 +0200
@@ -94,17 +94,17 @@
   @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
       split_conv unit_case_Unity} @ sum_prod_thms_map;
 
-fun mk_iter_tac pre_map_defs map_id's iter_defs ctor_iter ctr_def ctxt =
-  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_id's @
+fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt =
+  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @
     iter_unfold_thms) THEN HEADGOAL (rtac refl);
 
 val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
 
-fun mk_coiter_tac coiter_defs map_id's ctor_dtor_coiter pre_map_def ctr_def ctxt =
+fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
   HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN'
     asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE
-  (unfold_thms_tac ctxt (pre_map_def :: map_id's @ coiter_unfold_thms) THEN
+  (unfold_thms_tac ctxt (pre_map_def :: map_idents @ coiter_unfold_thms) THEN
    HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)));
 
 fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
diff -r 9228c575d67d -r c31c0c311cf0 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 14:17:19 2013 +0200
@@ -14,10 +14,6 @@
     Proof.state
 end;
 
-(* TODO:
-     - error handling for indirect calls
-*)
-
 structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
 struct
 
@@ -341,7 +337,7 @@
 
     val defs = build_defs lthy' bs funs_data rec_specs get_indices;
 
-    fun prove def_thms' {ctr_specs, nested_map_id's, nested_map_comps, ...} induct_thm fun_data
+    fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data
         lthy =
       let
         val fun_name = #fun_name (hd fun_data);
@@ -351,7 +347,7 @@
           |> map_filter (try (fn (x, [y]) =>
             (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
           |> map (fn (user_eqn, num_extra_args, rec_thm) =>
-            mk_primrec_tac lthy num_extra_args nested_map_id's nested_map_comps def_thms rec_thm
+            mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
             |> K |> Goal.prove lthy [] [] user_eqn)
 
         val notes =
diff -r 9228c575d67d -r c31c0c311cf0 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Fri Aug 30 14:17:19 2013 +0200
@@ -22,10 +22,10 @@
 open BNF_Util
 open BNF_Tactics
 
-fun mk_primrec_tac ctxt num_extra_args map_id's map_comps fun_defs recx =
+fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
   unfold_thms_tac ctxt fun_defs THEN
   HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
-  unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_id's) THEN
+  unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
   HEADGOAL (rtac refl);
 
 fun mk_primcorec_taut_tac ctxt =
@@ -54,10 +54,10 @@
 fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
   mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_id's map_comps =
+fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_idents map_comps =
   mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
   unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
-    maps @ map_comps @ map_id's) THEN HEADGOAL (rtac refl);
+    maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
 
 fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels =
   HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
diff -r 9228c575d67d -r c31c0c311cf0 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Aug 30 14:17:19 2013 +0200
@@ -35,7 +35,7 @@
 
   type rec_spec =
     {recx: term,
-     nested_map_id's: thm list,
+     nested_map_idents: thm list,
      nested_map_comps: thm list,
      ctr_specs: rec_ctr_spec list}
 
@@ -94,7 +94,7 @@
 
 type rec_spec =
   {recx: term,
-   nested_map_id's: thm list,
+   nested_map_idents: thm list,
    nested_map_comps: thm list,
    ctr_specs: rec_ctr_spec list};
 
@@ -336,7 +336,7 @@
 
     fun mk_spec {T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} =
       {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
-       nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
+       nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
        ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
   in