tuning

--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Mar 29 19:11:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Mar 29 19:17:05 2016 +0200
@@ -355,7 +355,7 @@
    corecUU_unique: thm,
    corecUU_transfer: thm,
    buffer: buffer,
-   all_dead_k_bnfs: BNF_Def.bnf list,
+   all_dead_k_bnfs: bnf list,
    Retr: term,
    equivp_Retr: thm,
    Retr_coinduct: thm,
@@ -2144,7 +2144,6 @@
     val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
     val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
     val dead_ssig_map = mk_map 1 As Bs (map_of_bnf dead_ssig_bnf);
-    val dead_ssig_rel = mk_rel 1 As Bs (rel_of_bnf dead_ssig_bnf);
 
     val ((Lam, Lam_def), lthy) = lthy
       |> define_Lam_base fp_b version Y Z preT ssig_T dead_pre_map Sig unsig dead_sig_map Oper
@@ -2384,7 +2383,6 @@
     val ssig_map = mk_mapN lthy live_AsBs ssig_T ssig_bnf;
     val ssig_rel = mk_relN lthy live_AsBs ssig_T ssig_bnf;
     val dead_ssig_map = mk_map 1 res_As res_Bs (map_of_bnf dead_ssig_bnf);
-    val dead_ssig_rel = mk_rel 1 res_As res_Bs (rel_of_bnf dead_ssig_bnf);
     val old_Lam = enforce_type lthy domain_type old_Lam_domT old_Lam0;
     val old_proto_sctr = enforce_type lthy domain_type preT old_proto_sctr0;
     val old_flat = enforce_type lthy range_type old_ssig_T old_flat0;
@@ -2409,7 +2407,6 @@
     val dead_pre_map_comp0 = map_comp0_of_bnf dead_pre_bnf;
     val dead_pre_map_comp = map_comp_of_bnf dead_pre_bnf;
     val fp_map_id = map_id_of_bnf fp_bnf;
-    val fp_rel_eq = rel_eq_of_bnf fp_bnf;
     val [ctor_dtor] = #ctor_dtors fp_res;
     val [dtor_inject] = #dtor_injects fp_res;
     val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res;

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 29 19:11:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 29 19:17:05 2016 +0200
@@ -20,8 +20,8 @@
   val build_corecUU_arg_and_goals: bool -> term -> term list * term -> local_theory ->
     (((thm list * thm list * thm list) * term list) * term) * local_theory
   val derive_eq_corecUU: Proof.context -> BNF_GFP_Grec.corec_info -> term -> term -> thm -> thm
-  val derive_unique: Proof.context -> morphism -> term -> BNF_GFP_Grec.corec_info -> typ -> thm ->
-    thm
+  val derive_unique: Proof.context -> morphism -> term -> BNF_GFP_Grec.corec_info -> string ->
+    thm -> thm
 
   val corec_cmd: corec_option list -> (binding * string option * mixfix) list * string ->
     local_theory -> local_theory
@@ -262,7 +262,7 @@
   let
     val SOME {casex, exhaust, case_thms, ...} = ctr_sugar_of ctxt fpT_name;
 
-    val fpT0 as Type (_, As0) = domain_type (body_fun_type (fastype_of casex));
+    val Type (_, As0) = domain_type (body_fun_type (fastype_of casex));
 
     val (As, _) = ctxt
       |> mk_TFrees' (map Type.sort_of_atyp As0);
@@ -321,7 +321,7 @@
   maps (#algrho_eqs o snd) (all_friend_extras_of ctxt);
 
 fun derive_code ctxt inner_fp_simps goal
-    {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs, corecUU_thm, ...} res_T fun_t
+    {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs, corecUU_thm, ...} fun_t
     fun_def =
   let
     val fun_T = fastype_of fun_t;
@@ -366,8 +366,8 @@
   end;
 
 fun derive_unique ctxt phi code_goal
-    {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs, corecUU_unique, ...}
-    (res_T as Type (fpT_name, _)) eq_corecUU =
+    {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs, corecUU_unique, ...} fpT_name
+    eq_corecUU =
   let
     val SOME {pre_bnf, fp_bnf, absT_info, fp_nesting_bnfs, live_nesting_bnfs, fp_ctr_sugar, ...} =
       fp_sugar_of ctxt fpT_name;
@@ -590,8 +590,8 @@
       ||>> mk_Frees "y" xy_Ts;
 
     fun mk_prem xy_T x y =
-      BNF_Def.build_rel [] ctxt [fpT]
-        (fn (T, _) => if T = fpT then Rcong else HOLogic.eq_const T) (xy_T, xy_T) $ x $ y;
+      build_rel [] ctxt [fpT] (fn (T, _) => if T = fpT then Rcong else HOLogic.eq_const T)
+        (xy_T, xy_T) $ x $ y;
 
     val prems = @{map 3} mk_prem xy_Ts xs ys;
     val concl = Rcong $ list_comb (alg, xs) $ list_comb (alg, ys);
@@ -1055,7 +1055,7 @@
           |> singleton (Type_Infer.fixate lthy)
           |> type_of
           |> dest_funT
-          |-> BNF_GFP_Grec_Sugar_Util.generalize_types 1
+          |-> generalize_types 1
           |> funT_of_tupleT m;
 
         val j = maxidx_of_typ deadfixed_T + 1;
@@ -2110,7 +2110,7 @@
 
         val lthy = lthy |> friend ? derive_and_note_friend_extra_theorems;
 
-        val code_thm = derive_code lthy inner_fp_simps code_goal corec_info res_T fun_t fun_def;
+        val code_thm = derive_code lthy inner_fp_simps code_goal corec_info fun_t fun_def;
 (* TODO:
         val ctr_thmss = map mk_thm (#2 views);
         val disc_thmss = map mk_thm (#3 views);
@@ -2119,8 +2119,10 @@
 *)
 
         val uniques =
-          if null inner_fp_simps then [derive_unique lthy phi (#1 views0) corec_info res_T fun_def]
-          else [];
+          if null inner_fp_simps then
+            [derive_unique lthy phi (#1 views0) corec_info fpT_name fun_def]
+          else
+            [];
 
 (* TODO:
         val disc_iff_or_disc_thmss =
@@ -2299,7 +2301,7 @@
           |> derive_and_update_coinduct_cong_intross [corec_info];
         val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
 
-        val unique = derive_unique lthy Morphism.identity code_goal corec_info res_T eq_corecUU;
+        val unique = derive_unique lthy Morphism.identity code_goal corec_info fpT_name eq_corecUU;
 
         val notes =
           [(codeN, [code_thm], []),

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML	Tue Mar 29 19:11:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML	Tue Mar 29 19:17:05 2016 +0200
@@ -55,6 +55,8 @@
         | NONE => error ("No corecursor for " ^ quote (Syntax.string_of_typ ctxt res_T) ^
           " (use " ^ quote (#1 @{command_keyword coinduction_upto}) ^ " to derive it)"));
 
+      val Type (fpT_name, _) = res_T;
+
       val parsed_eq = parse_corec_equation ctxt [fun_t] code_goal;
       val explored_eq =
         explore_corec_equation ctxt false false "" fun_t corec_parse_info res_T parsed_eq;
@@ -62,7 +64,7 @@
       val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_t explored_eq ctxt;
       val eq_corecUU = derive_eq_corecUU ctxt corec_info fun_t corecUU_arg code_thm;
 
-      val unique' = derive_unique ctxt Morphism.identity code_goal corec_info res_T eq_corecUU
+      val unique' = derive_unique ctxt Morphism.identity code_goal corec_info fpT_name eq_corecUU
         |> funpow num_args_in_concl (fn thm => thm RS fun_cong);
     in
       HEADGOAL ((K all_tac APPEND' rtac ctxt sym) THEN' rtac ctxt unique' THEN'