--- a/src/Pure/typedecl.ML Mon Nov 26 12:19:26 2007 +0100
+++ b/src/Pure/typedecl.ML Mon Nov 26 12:19:27 2007 +0100
@@ -2,7 +2,7 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Primitive type declarations.
+Type declarations with interpretation.
*)
signature TYPEDECL =
@@ -19,15 +19,15 @@
val _ = Context.add_setup TypedeclInterpretation.init;
-fun add (a, vs : string list, mx) thy =
+fun add (a, vs, mx) thy =
let
- val no_typargs = if not (has_duplicates (op =) vs) then length vs
- else error ("Duplicate parameters in type declaration: " ^ quote a);
+ val _ = has_duplicates (op =) vs andalso
+ error ("Duplicate parameters in type declaration: " ^ quote a);
val a' = Sign.full_name thy a;
val T = Type (a', map (fn v => TFree (v, [])) vs);
in
thy
- |> Sign.add_types [(a, no_typargs, mx)]
+ |> Sign.add_types [(a, length vs, mx)]
|> TypedeclInterpretation.data a'
|> pair T
end;