# HG changeset patch
# User blanchet
# Date 1380183623 -7200
# Node ID 54afdc258272bf098b607608d1f5748275e4218c
# Parent  d177eb989c65ffda6f7a3b21d19a7c2c23e0fe50
tuning

diff -r d177eb989c65 -r 54afdc258272 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 10:00:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 10:20:23 2013 +0200
@@ -272,13 +272,12 @@
     val sel_defaultss =
       pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
 
-    val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
-    val data_b_name = Long_Name.base_name dataT_name;
-    val data_b = Binding.name data_b_name;
+    val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
+    val fc_b_name = Long_Name.base_name fcT_name;
+    val fc_b = Binding.name fc_b_name;
 
     fun qualify mandatory =
-      Binding.qualify mandatory data_b_name o
-      (rep_compat ? Binding.qualify false rep_compat_prefix);
+      Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
 
     fun dest_TFree_or_TVar (TFree p) = p
       | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
@@ -291,7 +290,7 @@
 
     val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As;
 
-    val dataT = Type (dataT_name, As);
+    val fcT = Type (fcT_name, As);
     val ctrs = map (mk_ctr As) ctrs0;
     val ctr_Tss = map (binder_types o fastype_of) ctrs;
 
@@ -343,7 +342,7 @@
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
-      ||>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"]
+      ||>> (apfst (map (rpair fcT)) oo Variable.variant_fixes) [fc_b_name, fc_b_name ^ "'"]
       ||>> mk_Frees "z" [B]
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
 
@@ -366,7 +365,7 @@
       qualify false
         (if Binding.is_empty raw_case_binding orelse
             Binding.eq_name (raw_case_binding, standard_binding) then
-           Binding.suffix_name ("_" ^ caseN) data_b
+           Binding.suffix_name ("_" ^ caseN) fc_b
          else
            raw_case_binding);
 
@@ -422,7 +421,7 @@
         (true, [], [], [], [], [], [], [], [], [], lthy)
       else
         let
-          fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT);
+          fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
 
           fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
 
@@ -453,7 +452,7 @@
                     quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
                     ^ quote (Syntax.string_of_typ lthy T')));
             in
-              mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u,
+              mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
                 Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
             end;
 
@@ -822,7 +821,7 @@
           end;
 
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
-        val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
+        val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
 
         val notes =
           [(caseN, case_thms, code_nitpick_simp_simp_attrs),
@@ -866,7 +865,7 @@
                (fn phi => Case_Translation.register
                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
          |> Local_Theory.notes (notes' @ notes) |> snd
-         |> register_ctr_sugar dataT_name ctr_sugar)
+         |> register_ctr_sugar fcT_name ctr_sugar)
       end;
   in
     (goalss, after_qed, lthy')
diff -r d177eb989c65 -r 54afdc258272 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 10:00:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 10:20:23 2013 +0200
@@ -80,6 +80,8 @@
     (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
 
+(* TODO: do we need "collapses"? "distincts"? *)
+(* TODO: reduce code duplication with selector tactic above *)
 fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
   HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
   mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN