src/HOL/Library/rewrite.ML
changeset 60051 2a1cab4c9c9d
parent 60050 dc6ac152d864
child 60052 616a17640229
     1.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 12:18:47 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 14:45:44 2015 +0200
     1.3 @@ -307,7 +307,7 @@
     1.4            | subst _ t = t
     1.5        in Term.map_aterms (subst idents) end
     1.6  
     1.7 -    val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (map_filter I [to])
     1.8 +    val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
     1.9      val thm' = Thm.incr_indexes (maxidx + 1) thm
    1.10    in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end
    1.11    handle NO_TO_MATCH => NONE
    1.12 @@ -464,7 +464,7 @@
    1.13              fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
    1.14                | mk_free_constrs _ = []
    1.15  
    1.16 -            val ts = maps mk_free_constrs ps @ map_filter I [to]
    1.17 +            val ts = maps mk_free_constrs ps @ the_list to
    1.18                |> Syntax.check_terms (hole_syntax ctxt)
    1.19              val ctxt' = fold Variable.declare_term ts ctxt
    1.20              val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts