# HG changeset patch
# User blanchet
# Date 1457987869 -3600
# Node ID a1e73be79c0b15451208db0363818d773bfa45af
# Parent  d21dab28b3f9f6597c6c5cce1398dc778a094dfc
generalized ML function

diff -r d21dab28b3f9 -r a1e73be79c0b src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 14 15:58:02 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 14 21:37:49 2016 +0100
@@ -21,7 +21,7 @@
 
   exception BAD_DEAD of typ * typ
 
-  val bnf_of_typ: BNF_Def.inline_policy -> (binding -> binding) ->
+  val bnf_of_typ: bool -> BNF_Def.inline_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> (string * sort) list ->
     (string * sort) list -> typ -> (comp_cache * unfold_set) * local_theory ->
     (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
@@ -964,10 +964,10 @@
 
 exception BAD_DEAD of typ * typ;
 
-fun bnf_of_typ _ _ _ _ Ds0 (T as TFree T') accum =
+fun bnf_of_typ _ _ _ _ _ Ds0 (T as TFree T') accum =
     (if member (op =) Ds0 T' then (DEADID_bnf, ([T], [])) else (ID_bnf, ([], [T])), accum)
-  | bnf_of_typ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
-  | bnf_of_typ const_policy qualify' flatten_tyargs Xs Ds0 (T as Type (C, Ts))
+  | bnf_of_typ _ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
+  | bnf_of_typ optim const_policy qualify' flatten_tyargs Xs Ds0 (T as Type (C, Ts))
       (accum as (_, lthy)) =
     let
       fun check_bad_dead ((_, (deads, _)), _) =
@@ -982,7 +982,7 @@
       (case bnf_opt of
         NONE => ((DEADID_bnf, ([T], [])), accum)
       | SOME bnf =>
-        if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
+        if optim andalso forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
           let
             val T' = T_of_bnf bnf;
             val deads = deads_of_bnf bnf;
@@ -1007,8 +1007,8 @@
             val oDs = map (nth Ts) oDs_pos;
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
             val ((inners, (Dss, Ass)), (accum', lthy')) =
-              apfst (apsnd split_list o split_list)
-                (@{fold_map 2} (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
+              apfst (apsnd split_list o split_list) (@{fold_map 2}
+                (fn i => bnf_of_typ optim Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
                 (if length Ts' = 1 then [0] else 1 upto length Ts') Ts' accum);
           in
             compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
diff -r d21dab28b3f9 -r a1e73be79c0b src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 14 15:58:02 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 14 21:37:49 2016 +0100
@@ -626,7 +626,7 @@
     val ((bnfs, (deadss, livess)), accum) =
       apfst (apsnd split_list o split_list)
         (@{fold_map 2}
-          (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
+          (fn b => bnf_of_typ true Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
           ((empty_comp_cache, empty_unfolds), lthy));
 
     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
diff -r d21dab28b3f9 -r a1e73be79c0b src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Mon Mar 14 15:58:02 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Mon Mar 14 21:37:49 2016 +0100
@@ -79,7 +79,7 @@
 
     (* get the bnf for RepT *)
     val ((bnf, (deads, alphas)),((_, unfolds), lthy)) =
-      bnf_of_typ Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
+      bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
         Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy);
 
     val set_bs =