tuning

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 08 00:43:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 08 10:16:37 2016 +0200
@@ -306,7 +306,7 @@
             (fn {context = ctxt, prems = _} =>
               mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
           |> Thm.close_derivation)
-        (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
+        (map2 (curry mk_Trueprop_eq) sets sets_alt);
 
     fun map_cong0_tac ctxt =
       mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer)

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 08 00:43:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 08 10:16:37 2016 +0200
@@ -2303,14 +2303,6 @@
                 register_hint ())
           end);
 
-    val abss = map #abs absT_infos;
-    val reps = map #rep absT_infos;
-    val absTs = map #absT absT_infos;
-    val repTs = map #repT absT_infos;
-    val abs_injects = map #abs_inject absT_infos;
-    val abs_inverses = map #abs_inverse absT_infos;
-    val type_definitions = map #type_definition absT_infos;
-
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
 
@@ -2328,6 +2320,7 @@
     val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
     val live_nesting_rel_eq_onps = map rel_eq_onp_of_bnf live_nesting_bnfs;
 
+    val liveness = liveness_of_fp_bnf num_As any_fp_bnf;
     val live = live_of_bnf any_fp_bnf;
     val _ =
       if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs @ pred_bs) then
@@ -2335,14 +2328,21 @@
       else
         ();
 
-    val Bs =
-      @{map 3} (fn alive => fn A as TFree (_, S) => fn B =>
-          if alive then resort_tfree_or_tvar S B else A)
-        (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
+    val Bs = @{map 3} (fn alive => fn A as TFree (_, S) => fn B =>
+        if alive then resort_tfree_or_tvar S B else A)
+      liveness As Bs0;
 
     val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
     val live_AsBs = filter (op <>) (As ~~ Bs);
 
+    val abss = map #abs absT_infos;
+    val reps = map #rep absT_infos;
+    val absTs = map #absT absT_infos;
+    val repTs = map #repT absT_infos;
+    val abs_injects = map #abs_inject absT_infos;
+    val abs_inverses = map #abs_inverse absT_infos;
+    val type_definitions = map #type_definition absT_infos;
+
     val ctors = map (mk_ctor As) ctors0;
     val dtors = map (mk_dtor As) dtors0;
 
@@ -2454,10 +2454,8 @@
           fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy);
 
           val maps0 = map map_of_bnf fp_bnfs;
-          val ABs = As ~~ Bs
-          val liveness = map (op <>) ABs;
           val f_names = variant_names num_As "f";
-          val fs = map2 (curry Free) f_names (map (op -->) ABs);
+          val fs = map2 (curry Free) f_names (map (op -->) (As ~~ Bs));
           val live_gs = AList.find (op =) (fs ~~ liveness) true;
 
           val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
@@ -2474,7 +2472,7 @@
 
           val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) grecs gmaps;
 
-          val ABfs = ABs ~~ fs;
+          val ABfs = (As ~~ Bs) ~~ fs;
 
           fun mk_rec_arg_arg (x as Free (_, T)) =
             let val U = B_ify_T T in
@@ -2607,11 +2605,10 @@
       else
         let
           fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
+
           val maps0 = map map_of_bnf fp_bnfs;
-          val ABs = As ~~ Bs
-          val liveness = map (op <>) ABs;
           val f_names = variant_names num_As "f";
-          val fs = map2 (curry Free) f_names (map (op -->) ABs);
+          val fs = map2 (curry Free) f_names (map (op -->) (As ~~ Bs));
           val live_fs = AList.find (op =) (fs ~~ liveness) true;
 
           val fmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_fs)) maps0;
@@ -2628,7 +2625,7 @@
 
           val map_o_corec_lhss = map2 (curry HOLogic.mk_comp) fmaps gcorecs;
 
-          val ABgs = ABs ~~ fs;
+          val ABfs = (As ~~ Bs) ~~ fs;
 
           fun mk_map_o_corec_arg corec_argB_T g =
             let
@@ -2636,7 +2633,7 @@
               val U = range_type corec_argB_T;
             in
               if T = U then g
-              else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U), g)
+              else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABfs) (T, U), g)
             end;
 
           fun mk_map_o_corec_rhs corecx =

--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Thu Sep 08 00:43:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Thu Sep 08 10:16:37 2016 +0200
@@ -13,7 +13,6 @@
   val substT: typ -> typ -> term -> term
   val freeze_types: Proof.context -> (indexname * sort) list -> typ list -> typ list
   val dummify_atomic_types: term -> term
-  val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term
   val define_const: bool -> binding -> int -> string -> term -> local_theory ->
     (term * thm) * local_theory
 
@@ -213,9 +212,6 @@
 
 val dummify_atomic_types = Term.map_types (Term.map_atyps (K Term.dummyT));
 
-fun enforce_type ctxt get_T T t =
-  Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t;
-
 fun mk_internal internal ctxt f =
   if internal andalso not (Config.get ctxt bnf_internals) then f else I
 fun mk_fp_binding fp_b pre = Binding.map_name (K pre) fp_b

--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 08 00:43:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 08 10:16:37 2016 +0200
@@ -36,6 +36,8 @@
   val snd_const: typ -> term
   val Id_const: typ -> term
 
+  val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term
+
   val mk_Ball: term -> term -> term
   val mk_Bex: term -> term -> term
   val mk_Card_order: term -> term
@@ -221,6 +223,9 @@
 
 (** Operators **)
 
+fun enforce_type ctxt get_T T t =
+  Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t;
+
 fun mk_converse R =
   let
     val RT = dest_relT (fastype_of R);