# HG changeset patch
# User haftmann
# Date 1338731395 -7200
# Node ID 04aeda922be240dc3dc1e5a79c498c48fb3b074d
# Parent  9f458b3efb5c2351d01f1a1d2ea2eed4f3339882
explicit check for correct number of arguments for abstract constructor

diff -r 9f458b3efb5c -r 04aeda922be2 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Jun 02 08:32:42 2012 +0200
+++ b/src/Pure/Isar/code.ML	Sun Jun 03 15:49:55 2012 +0200
@@ -637,6 +637,9 @@
       then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
     val _ = check_decl_ty thy (abs, raw_ty);
     val _ = check_decl_ty thy (rep, rep_ty);
+    val _ = if length (binder_types raw_ty) = 1
+      then ()
+      else bad "Bad type for abstract constructor";
     val _ = (fst o dest_Var) param
       handle TERM _ => bad "Not an abstype certificate";
     val _ = if param = rhs then () else bad "Not an abstype certificate";