# HG changeset patch # User blanchet # Date 1369789826 -7200 # Node ID 689062704416e5f856150d4cab38beae2bed6b92 # Parent b6a0668211f6911804bbcc850795c26e0f4478f7 tuning diff -r b6a0668211f6 -r 689062704416 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed May 29 02:35:49 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed May 29 03:10:26 2013 +0200 @@ -681,30 +681,15 @@ val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs); - (* ### *) - fun typ_subst inst (T as Type (s, Ts)) = - (case AList.lookup (op =) inst T of - NONE => Type (s, map (typ_subst inst) Ts) - | SOME T' => T') - | typ_subst inst T = the_default T (AList.lookup (op =) inst T); - - fun mk_U' maybe_mk_prodT = - typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs); - - (* ### *) - fun build_rec_like fiters maybe_tick (T, U) = - if T = U then - id_const T - else - (case find_index (curry (op =) T) fpTs of - ~1 => build_map lthy (build_rec_like fiters maybe_tick) (T, U) - | kk => maybe_tick (nth us kk) (nth fiters kk)); + 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_rec_like fiters maybe_tick (T, mk_U' maybe_mk_prodT 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 tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));