# HG changeset patch # User blanchet # Date 1370424624 -7200 # Node ID 4a4da43e855ac189d4700766ac999905ce636958 # Parent 085771de5720784a9e2ede8df5b86f0918c0c22b tuning diff -r 085771de5720 -r 4a4da43e855a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Jun 05 11:16:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Jun 05 11:30:24 2013 +0200 @@ -253,13 +253,6 @@ val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of; -fun meta_unzip_rec getT left right nested fpTs y = - let val T = getT y in - if member (op =) fpTs T then [left y, right y] - else if exists_subtype_in fpTs T then [nested y] - else [y] - end; - fun project_co_recT special_Tname Cs proj = let fun project (Type (s, Ts as [T, U])) = @@ -683,13 +676,16 @@ fun mk_nested_U maybe_mk_prodT = typ_subst_nonatomic (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs); - fun unzip_iters fiters maybe_tick maybe_mk_prodT = - meta_unzip_rec (snd o dest_Free) I - (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (K o nth fiters)) - (T, mk_U T) $ x) - (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (fn kk => fn _ => - maybe_tick (nth us kk) (nth fiters kk))) (T, mk_nested_U maybe_mk_prodT T) $ x) - fpTs; + fun unzip_iters fiters maybe_tick maybe_mk_prodT x = + let val Free (_, T) = x in + if member (op =) fpTs T then + [x, build_map lthy (indexify_fst fpTs (K o nth fiters)) (T, mk_U T) $ x] + else if exists_subtype_in fpTs T then + [build_map lthy (indexify_fst fpTs (fn kk => fn _ => + maybe_tick (nth us kk) (nth fiters kk))) (T, mk_nested_U maybe_mk_prodT T) $ x] + else + [x] + end; fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));