Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/coherent.ML
changeset 74282 c2ee8d993d6a
parent 67522 9e712280cc37 
--- a/src/Tools/coherent.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/coherent.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -175,13 +175,14 @@
     val _ =
       cond_trace ctxt (fn () =>
         Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms)));
+    val instT = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye);
+    val inst =
+      map (fn (ixn, (T, t)) =>
+        ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @
+      map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts;
     val th' =
       Drule.implies_elim_list
-        (Thm.instantiate
-           (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye),
-            map (fn (ixn, (T, t)) =>
-              ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @
-            map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th)
+        (Thm.instantiate (TVars.make instT, Vars.make inst) th)
         (map (nth asms) is);
     val (_, cases) = dest_elim (Thm.prop_of th');
   in
isabelle