# HG changeset patch # User noschinl # Date 1428929144 -7200 # Node ID 2a1cab4c9c9d6b667753de0b1d57c28b8d700d07 # Parent dc6ac152d8643c876d0280c0452a101e982f338c tuned diff -r dc6ac152d864 -r 2a1cab4c9c9d src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Mon Apr 13 12:18:47 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Mon Apr 13 14:45:44 2015 +0200 @@ -307,7 +307,7 @@ | subst _ t = t in Term.map_aterms (subst idents) end - val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (map_filter I [to]) + val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to) val thm' = Thm.incr_indexes (maxidx + 1) thm in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end handle NO_TO_MATCH => NONE @@ -464,7 +464,7 @@ fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs | mk_free_constrs _ = [] - val ts = maps mk_free_constrs ps @ map_filter I [to] + val ts = maps mk_free_constrs ps @ the_list to |> Syntax.check_terms (hole_syntax ctxt) val ctxt' = fold Variable.declare_term ts ctxt val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts