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.
Improved well-formedness check.
authorberghofe
Thu, 06 Aug 1998 17:51:03 +0200
changeset 5279 cba6a96f5812
parent 5278 a903b66822e2
child 5280 6055775a151b
Improved well-formedness check.
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_package.ML	Thu Aug 06 15:48:13 1998 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Aug 06 17:51:03 1998 +0200
@@ -579,7 +579,11 @@
     fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
       let
         fun prep_constr ((constrs, constr_syntax', sorts'), (cname, mx', cargs)) =
-          let val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs)
+          let
+            val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
+            val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
+                [] => ()
+              | vs => error ("Extra type variables on rhs: " ^ commas vs))
           in (constrs @ [((if length dts = 1 then Sign.full_name sign
                else Sign.full_name_path sign (Sign.base_name tname))
                  (Syntax.const_name cname mx'),
isabelle