# 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