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/Pure/theory.ML
changeset 74279 42db84eaee2d
parent 74278 a123db647573
child 74339 bff865939cc3 
--- a/src/Pure/theory.ML	Thu Sep 09 22:12:05 2021 +0200
+++ b/src/Pure/theory.ML	Thu Sep 09 22:29:15 2021 +0200
@@ -247,7 +247,7 @@
     val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs));
     val rhs_extras =
       TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd))
-      |> TFrees.list_set_rev;
+      |> TFrees.keys;
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
isabelle