# HG changeset patch
# User blanchet
# Date 1473249196 -7200
# Node ID 076129f60a3120a63f764873437609a68ed3a7e6
# Parent  5f8643e8ced5a968819eb58113eb32029e222c0c
tuned whitespace

diff -r 5f8643e8ced5 -r 076129f60a31 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 06 21:36:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 07 13:53:16 2016 +0200
@@ -2113,8 +2113,7 @@
 
     val fake_Ts = map (fn s => Type (s, As)) fake_T_names;
 
-    val ((((Bs0, Cs), Es), Xs), _) =
-      no_defs_lthy
+    val ((((Bs0, Cs), Es), Xs), _) = no_defs_lthy
       |> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
       |> mk_TFrees num_As
       ||>> mk_TFrees nn
@@ -2170,10 +2169,9 @@
         (As ~~ transpose set_boss);
 
     val (((pre_bnfs, absT_infos), _), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
-             dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
-             ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
-             xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
-             xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
+             dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors, ctor_dtors,
+             ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels, xtor_co_rec_thms,
+             xtor_rel_co_induct, dtor_set_inducts, xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
       fixpoint_bnf false I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
         (map dest_TFree As) (map dest_TFree killed_As) (map dest_TFree Xs) ctrXs_repTs
diff -r 5f8643e8ced5 -r 076129f60a31 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Sep 06 21:36:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Sep 07 13:53:16 2016 +0200
@@ -325,9 +325,9 @@
             (case find_first (fn f => body_fun_type (fastype_of f) = TU) un_folds of
               NONE => force_fold i TU (nth fp_un_folds i)
             | SOME f => f);
-  
+
           val TUs = binder_fun_types (fastype_of TUfold);
-  
+
           fun mk_s TU' cache_lthy =
             let
               val i = find_index (fn T => co_alg_argT TU' = T) Xs;
diff -r 5f8643e8ced5 -r 076129f60a31 src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Tue Sep 06 21:36:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Wed Sep 07 13:53:16 2016 +0200
@@ -26,7 +26,7 @@
 
 val vimage2p_unfolds = o_apply :: @{thms vimage2p_def};
 
-fun unfold_at_most_once_tac ctxt thms = 
+fun unfold_at_most_once_tac ctxt thms =
   CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt);
 val unfold_once_tac = CHANGED ooo unfold_at_most_once_tac;
 
diff -r 5f8643e8ced5 -r 076129f60a31 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 06 21:36:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Sep 07 13:53:16 2016 +0200
@@ -668,7 +668,7 @@
         val T = range_type (fastype_of rhs);
       in
         HOLogic.mk_eq (HOLogic.id_const T, rhs)
-      end; 
+      end;
     val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map mk_goal un_folds));
     fun mk_inverses NONE = []
       | mk_inverses (SOME (src, dst)) =
@@ -883,10 +883,10 @@
               #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of
               #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T'))
             Ts Us xtor_un_fold_transfers;
-      
+
           fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs
             xtor_un_fold_transfers map_transfers xtor_rels;
-      
+
           val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum;
           val rec_phis =
             map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis;