mutual instances

--- a/src/Pure/Isar/class_target.ML	Mon Jun 29 16:17:56 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Mon Jun 29 16:17:57 2009 +0200
@@ -32,6 +32,7 @@
   (*instances*)
   val init_instantiation: string list * (string * sort) list * sort
     -> theory -> local_theory
+  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
   val instantiation_instance: (local_theory -> local_theory)
     -> local_theory -> Proof.state
   val prove_instantiation_instance: (Proof.context -> tactic)
@@ -44,7 +45,8 @@
   val instantiation_param: local_theory -> binding -> string option
   val confirm_declaration: binding -> local_theory -> local_theory
   val pretty_instantiation: local_theory -> Pretty.T
-  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
+  val read_multi_arity: theory -> xstring list * xstring list * xstring
+    -> string list * (string * sort) list * sort
   val type_name: string -> string
 
   (*subclasses*)
@@ -419,6 +421,15 @@
   |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
   |> Option.map (fst o fst);
 
+fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
+  let
+    val all_arities = map (fn raw_tyco => Sign.read_arity thy
+      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
+    val tycos = map #1 all_arities;
+    val (_, sorts, sort) = hd all_arities;
+    val vs = Name.names Name.context Name.aT sorts;
+  in (tycos, vs, sort) end;
+
 
 (* syntax *)
 
@@ -578,15 +589,17 @@
 
 (* simplified instantiation interface with no class parameter *)
 
-fun instance_arity_cmd arities thy =
+fun instance_arity_cmd raw_arities thy =
   let
+    val (tycos, vs, sort) = read_multi_arity thy raw_arities;
+    val sorts = map snd vs;
+    val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
     fun after_qed results = ProofContext.theory
       ((fold o fold) AxClass.add_arity results);
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
-        o Logic.mk_arities o Sign.read_arity thy) arities)
+    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
   end;
 
 

--- a/src/Pure/Isar/isar_syn.ML	Mon Jun 29 16:17:56 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 29 16:17:57 2009 +0200
@@ -465,7 +465,7 @@
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.arity >> Class.instance_arity_cmd)
+    P.multi_arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof)
   || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 

--- a/src/Pure/Isar/theory_target.ML	Mon Jun 29 16:17:56 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Jun 29 16:17:57 2009 +0200
@@ -330,15 +330,6 @@
        else I)}
 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
 
-fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
-  let
-    val all_arities = map (fn raw_tyco => Sign.read_arity thy
-      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
-    val tycos = map #1 all_arities;
-    val (_, sorts, sort) = hd all_arities;
-    val vs = Name.names Name.context Name.aT sorts;
-  in (tycos, vs, sort) end;
-
 fun gen_overloading prep_const raw_ops thy =
   let
     val ctxt = ProofContext.init thy;
@@ -356,7 +347,7 @@
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
 fun instantiation_cmd raw_arities thy =
-  instantiation (read_multi_arity thy raw_arities) thy;
+  instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
 val overloading_cmd = gen_overloading Syntax.read_term;