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