# HG changeset patch
# User wenzelm
# Date 1630787208 -7200
# Node ID ef74cf118da3c1f79c01a9536c20eb7eb654ab7f
# Parent  dbaed92fd8afcf9c6678f462822330ece7c60518
clarified;

diff -r dbaed92fd8af -r ef74cf118da3 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Sep 04 22:17:15 2021 +0200
+++ b/src/Pure/theory.ML	Sat Sep 04 22:26:48 2021 +0200
@@ -246,8 +246,8 @@
 
     val lhs_vars = Term_Subst.TFrees.build (snd lhs |> fold Term_Subst.add_tfreesT);
     val rhs_extras =
-      fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
-        if Term_Subst.TFrees.defined lhs_vars v then I else insert (op =) v)) rhs [];
+      build (rhs |> fold (#2 #> (fold o Term.fold_atyps)
+        (fn TFree v => not (Term_Subst.TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^