# HG changeset patch
# User wenzelm
# Date 1404559313 -7200
# Node ID 3ad1b289f21b2afd3c4746ace3889279bf3cbf40
# Parent  f4904e2b3040bbad0c9497ad4d0159a46a276804
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);

diff -r f4904e2b3040 -r 3ad1b289f21b src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sat Jul 05 12:04:25 2014 +0200
+++ b/src/Pure/defs.ML	Sat Jul 05 13:21:53 2014 +0200
@@ -142,7 +142,7 @@
   err ctxt (c, args) (d, Us) "Circular" "";
 
 fun wellformed ctxt defs (c, args) (d, Us) =
-  forall is_TVar Us orelse
+  plain_args Us orelse
   (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
     SOME (Ts, description) =>
       err ctxt (c, args) (d, Us) "Malformed"