--- a/src/Pure/theory.ML Thu Sep 09 21:44:11 2021 +0200
+++ b/src/Pure/theory.ML Thu Sep 09 22:12:05 2021 +0200
@@ -244,10 +244,10 @@
[] => (item, map Logic.varifyT_global args)
| vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
- val lhs_vars = TFrees.build (snd lhs |> fold TFrees.add_tfreesT);
+ val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs));
val rhs_extras =
- build (rhs |> fold (#2 #> (fold o Term.fold_atyps)
- (fn TFree v => not (TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
+ TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd))
+ |> TFrees.list_set_rev;
val _ =
if null rhs_extras then ()
else error ("Specification depends on extra type variables: " ^