src/Tools/coherent.ML
changeset 32035 8e77b6a250d5
parent 31855 7c2a5e79a654
child 32091 30e2ffbba718
     1.1 --- a/src/Tools/coherent.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/Tools/coherent.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4    let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
     1.5      valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
     1.6        let val cs' = map (fn (Ts, ts) =>
     1.7 -        (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
     1.8 +        (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
     1.9        in
    1.10          inst_extra_vars ctxt dom cs' |>
    1.11            Seq.map_filter (fn (inst, cs'') =>
    1.12 @@ -184,7 +184,7 @@
    1.13              (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
    1.14                 (Vartab.dest tye),
    1.15            map (fn (ixn, (T, t)) =>
    1.16 -            (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
    1.17 +            (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
    1.18               Thm.cterm_of thy t)) (Vartab.dest env) @
    1.19            map (fn (ixnT, t) =>
    1.20              (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)