--- 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: " ^