Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
authorwenzelm
Sat, 05 Jul 2014 13:21:53 +0200
changeset 57520 3ad1b289f21b
parent 57517 f4904e2b3040
child 57521 b14c0794f97f
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
src/Pure/defs.ML file | annotate | diff | comparison | revisions 
--- 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"
isabelle