# HG changeset patch # User wenzelm # Date 1237316037 -3600 # Node ID e6a55291102e6685be0f928ebdb49f04275102d8 # Parent cd8e20f86795407690a71c1c81224605827d7b8f strip_abss: always strip abstractions as far as possible, without keeping alternatives (which appear to be redundant anyway, but cause significant slowdown since discrimination nets collapse abstractions); diff -r cd8e20f86795 -r e6a55291102e src/Pure/consts.ML --- a/src/Pure/consts.ML Tue Mar 17 19:06:04 2009 +0100 +++ b/src/Pure/consts.ML Tue Mar 17 19:53:57 2009 +0100 @@ -73,7 +73,7 @@ val empty_abbrevs = Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1; fun insert_abbrevs mode abbrs = - Symtab.map_default (mode, empty_abbrevs) (fold Item_Net.insert abbrs); + Symtab.map_default (mode, empty_abbrevs) (Item_Net.insert abbrs); fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes = let val nets = map_filter (Symtab.lookup rev_abbrevs) modes @@ -258,20 +258,16 @@ local -fun strip_abss tm = ([], tm) :: - (case tm of - Abs (a, T, t) => - if Term.loose_bvar1 (t, 0) then - strip_abss t |> map (fn (xs, b) => ((a, T) :: xs, b)) - else [] - | _ => []); +fun strip_abss (t as Abs (x, T, b)) = + if Term.loose_bvar1 (b, 0) then strip_abss b |>> cons (x, T) + else ([], t) + | strip_abss t = ([], t); fun rev_abbrev lhs rhs = let - fun abbrev (xs, body) = - let val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) [] - in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end; - in map abbrev (strip_abss (Envir.beta_eta_contract rhs)) end; + val (xs, body) = strip_abss (Envir.beta_eta_contract rhs); + val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []; + in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end; in