unified arity parser/arguments;

--- a/src/HOL/Tools/datatype_codegen.ML	Fri Feb 16 19:19:19 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Feb 16 22:13:15 2007 +0100
@@ -25,11 +25,11 @@
   val the_codetypes_mut_specs: theory -> (string * bool) list
     -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
   val get_codetypes_arities: theory -> (string * bool) list -> sort
-    -> (string * (((string * sort list) * sort) * term list)) list option
+    -> (string * (arity * term list)) list option
   val prove_codetypes_arities: tactic -> (string * bool) list -> sort
-    -> (((string * sort list) * sort) list -> (string * term list) list -> theory
+    -> (arity list -> (string * term list) list -> theory
     -> ((bstring * Attrib.src list) * term) list * theory)
-    -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
+    -> (arity list -> (string * term list) list -> theory -> theory)
     -> theory -> theory
 
   val setup: theory -> theory
@@ -584,11 +584,10 @@
           (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
       in (c, tys') end;
     val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto;
-    fun mk_arity tyco =
-      ((tyco, map snd vs), sort);
+    fun mk_arity tyco = (tyco, map snd vs, sort);
     fun typ_of_sort ty =
       let
-        val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
+        val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css;
       in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
     fun mk_cons tyco (c, tys) =
       let
@@ -605,7 +604,7 @@
   case get_codetypes_arities thy tycos sort
    of NONE => thy
     | SOME insts => let
-        fun proven ((tyco, asorts), sort) =
+        fun proven (tyco, asorts, sort) =
           Sorts.of_sort (Sign.classes_of thy)
             (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
         val (arities, css) = (split_list o map_filter

--- a/src/Pure/Isar/isar_syn.ML	Fri Feb 16 19:19:19 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 16 22:13:15 2007 +0100
@@ -113,8 +113,7 @@
 
 val aritiesP =
   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
-    (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
-      >> (Toplevel.theory o fold AxClass.axiomatize_arity));
+    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
 
 
 (* consts and syntax *)
@@ -406,19 +405,13 @@
 
 local
 
-val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
-
 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
 
-val parse_arity =
-  (P.xname --| P.$$$ "::" -- P.!!! P.arity)
-    >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
-
 in
 
 val classP =
-  OuterSyntax.command classK "define type class" K.thy_decl (
+  OuterSyntax.command "class" "define type class" K.thy_decl (
     P.name --| P.$$$ "="
     -- (
       class_subP --| P.$$$ "+" -- class_bodyP
@@ -430,17 +423,17 @@
           (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
 
 val instanceP =
-  OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
+  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
            >> ClassPackage.instance_class_cmd
       || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
            >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
-      || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
+      || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
            >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val print_classesP =
-  OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
+  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
       o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
 

--- a/src/Pure/Isar/outer_parse.ML	Fri Feb 16 19:19:19 2007 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Feb 16 22:13:15 2007 +0100
@@ -55,7 +55,7 @@
   val path: token list -> Path.T * token list
   val parname: token list -> string * token list
   val sort: token list -> string * token list
-  val arity: token list -> (string list * string) * token list
+  val arity: token list -> (string * string list * string) * token list
   val type_args: token list -> string list * token list
   val typ: token list -> string * token list
   val mixfix: token list -> mixfix * token list
@@ -202,7 +202,8 @@
 
 val sort = group "sort" xname;
 
-val arity = Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort;
+val arity = xname -- ($$$ "::" |-- !!!
+  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
 
 
 (* types *)

--- a/src/Pure/Tools/class_package.ML	Fri Feb 16 19:19:19 2007 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Feb 16 22:13:15 2007 +0100
@@ -13,13 +13,12 @@
     string * Proof.context
   val class_cmd: bstring -> string list -> Element.context Locale.element list -> theory ->
     string * Proof.context
-  val instance_arity: ((bstring * sort list) * sort) list
-    -> ((bstring * Attrib.src list) * term) list
+  val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
     -> theory -> Proof.state
-  val instance_arity_cmd: ((bstring * string list) * string) list
+  val instance_arity_cmd: (bstring * string list * string) list
     -> ((bstring * Attrib.src list) * string) list
     -> theory -> Proof.state
-  val prove_instance_arity: tactic -> ((string * sort list) * sort) list
+  val prove_instance_arity: tactic -> arity list
     -> ((bstring * Attrib.src list) * term) list
     -> theory -> theory
   val instance_class: class * class -> theory -> Proof.state
@@ -28,9 +27,7 @@
   val instance_sort_cmd: string * string -> theory -> Proof.state
   val prove_instance_sort: tactic -> class * sort -> theory -> theory
 
-  val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
-  val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a
-    (*'a must not keep any reference to theory*)
+  val assume_arities_of_sort: theory -> arity list -> typ * sort -> bool
 
   (* experimental class target *)
   val class_of_locale: theory -> string -> class option
@@ -113,16 +110,10 @@
   let
     val pp = Sign.pp thy;
     val algebra = Sign.classes_of thy
-      |> fold (fn ((tyco, asorts), sort) =>
+      |> fold (fn (tyco, asorts, sort) =>
            Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
   in Sorts.of_sort algebra ty_sort end;
 
-fun assume_arities_thy thy arities f =
-  let
-    val thy_read = (fold (fn ((tyco, asorts), sort)
-      => Sign.primitive_arity (tyco, asorts, sort)) arities o Theory.copy) thy
-  in f thy_read end;
-
 
 (* instances with implicit parameter handling *)
 
@@ -144,9 +135,7 @@
 
 fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
   let
-    fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort);
-    val arities = map prep_arity' raw_arities;
-    val arities_pair = map (fn (tyco, asorts, sort) => ((tyco, asorts), sort)) arities;
+    val arities = map (prep_arity theory) raw_arities;
     val _ = if null arities then error "at least one arity must be given" else ();
     val _ = case (duplicates (op =) o map #1) arities
      of [] => ()
@@ -187,7 +176,9 @@
               | SOME norm => map_types norm t
           in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
       in fold_map read defs cs end;
-    val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs);
+    val (defs, _) = read_defs raw_defs cs
+      (fold Sign.primitive_arity arities (Theory.copy theory));
+
     fun get_remove_contraint c thy =
       let
         val ty = Sign.the_const_constraint thy c;
@@ -272,7 +263,7 @@
 
 val ancestry = Graph.all_succs o fst o ClassData.get;
 
-fun param_map thy = 
+fun param_map thy =
   let
     fun params thy class =
       let