# HG changeset patch
# User wenzelm
# Date 1196075967 -3600
# Node ID 40d8409146f0dd200f6b910df1afbd0e37746be6
# Parent  0ca80ce89001cb7a0652f63e8005c1ee33ffb578
tuned comments;
tuned;

diff -r 0ca80ce89001 -r 40d8409146f0 src/Pure/typedecl.ML
--- 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;