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"