# HG changeset patch
# User haftmann
# Date 1350544620 -7200
# Node ID 2df2786ac7b70f5ed940abed00de2dfd8740ac60
# Parent  9d2da7f5945a8320b7cd196c2c479a68442ea7cd
no sort constraints on datatype constructors in internal bookkeeping

diff -r 9d2da7f5945a -r 2df2786ac7b7 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Oct 17 22:57:28 2012 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 18 09:17:00 2012 +0200
@@ -372,29 +372,24 @@
     val (_, vs) = last_typ (c, ty) ty;
   in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
 
-fun constrset_of_consts thy cs =
+fun constrset_of_consts thy consts =
   let
     val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
-      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
-    fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
-      let
-        val _ = if (tyco' : string) <> tyco
-          then error "Different type constructors in constructor set"
-          else ();
-        val sorts'' =
-          map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
-      in ((tyco, sorts''), c :: cs) end;
+      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts;
+    val raw_constructors = map (analyze_constructor thy) consts;
+    val tyco = case distinct (op =) (map (fst o fst) raw_constructors)
+     of [tyco] => tyco
+      | [] => error "Empty constructor set"
+      | tycos => error ("Different type constructors in constructor set: " ^ commas_quote tycos)
+    val vs = Name.invent Name.context Name.aT (Sign.arity_number thy tyco);
     fun inst vs' (c, (vs, ty)) =
       let
         val the_v = the o AList.lookup (op =) (vs ~~ vs');
-        val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
-        val (vs'', _) = typscheme thy (c, ty');
-      in (c, (vs'', binder_types ty')) end;
-    val c' :: cs' = map (analyze_constructor thy) cs;
-    val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
-    val vs = Name.invent_names Name.context Name.aT sorts;
-    val cs''' = map (inst vs) cs'';
-  in (tyco, (vs, rev cs''')) end;
+        val ty' = map_type_tfree (fn (v, _) => TFree (the_v v, [])) ty;
+        val (vs'', ty'') = typscheme thy (c, ty');
+      in (c, (vs'', binder_types ty'')) end;
+    val constructors = map (inst vs o snd) raw_constructors;
+  in (tyco, (map (rpair []) vs, constructors)) end;
 
 fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
  of (_, entry) :: _ => SOME entry