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/IsaPlanner/rw_inst.ML
changeset 77808 b43ee37926a9
parent 74282 c2ee8d993d6a
child 77863 760515c45864 
--- a/src/Tools/IsaPlanner/rw_inst.ML	Mon Apr 10 20:51:01 2023 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Mon Apr 10 22:38:18 2023 +0200
@@ -64,7 +64,8 @@
        bound vars with binders outside the redex *)
 
     val ns =
-      IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts);
+      IsaND.variant_names ctxt (Thm.full_prop_of rule :: Termset.dest (Thm.hyps_of rule))
+        (map fst Ts);
 
     val (fromnames, tonames, Ts') =
       fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>
isabelle