clarified;
authorwenzelm
Sat, 04 Sep 2021 22:26:48 +0200
changeset 74236 ef74cf118da3
parent 74235 dbaed92fd8af
child 74237 4426b52eabb4
clarified;
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: " ^