# HG changeset patch
# User berghofe
# Date 902418663 -7200
# Node ID cba6a96f581201399ca0ee986e9ff0a09aee00b4
# Parent  a903b66822e2f16fbb705cc599388a4d1b40c6b8
Improved well-formedness check.

diff -r a903b66822e2 -r cba6a96f5812 src/HOL/Tools/datatype_package.ML
--- 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'),