Improved well-formedness check.
authorberghofe
Thu Aug 06 17:51:03 1998 +0200 (1998-08-06)
changeset 5279cba6a96f5812
parent 5278 a903b66822e2
child 5280 6055775a151b
Improved well-formedness check.
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Aug 06 15:48:13 1998 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Aug 06 17:51:03 1998 +0200
     1.3 @@ -579,7 +579,11 @@
     1.4      fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
     1.5        let
     1.6          fun prep_constr ((constrs, constr_syntax', sorts'), (cname, mx', cargs)) =
     1.7 -          let val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs)
     1.8 +          let
     1.9 +            val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
    1.10 +            val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
    1.11 +                [] => ()
    1.12 +              | vs => error ("Extra type variables on rhs: " ^ commas vs))
    1.13            in (constrs @ [((if length dts = 1 then Sign.full_name sign
    1.14                 else Sign.full_name_path sign (Sign.base_name tname))
    1.15                   (Syntax.const_name cname mx'),