1.1 --- a/src/Pure/Isar/class_target.ML	Mon Jun 29 16:17:56 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Mon Jun 29 16:17:57 2009 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    (*instances*)
     1.5    val init_instantiation: string list * (string * sort) list * sort
     1.6      -> theory -> local_theory
     1.7 +  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
     1.8    val instantiation_instance: (local_theory -> local_theory)
     1.9      -> local_theory -> Proof.state
    1.10    val prove_instantiation_instance: (Proof.context -> tactic)
    1.11 @@ -44,7 +45,8 @@
    1.12    val instantiation_param: local_theory -> binding -> string option
    1.13    val confirm_declaration: binding -> local_theory -> local_theory
    1.14    val pretty_instantiation: local_theory -> Pretty.T
    1.15 -  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
    1.16 +  val read_multi_arity: theory -> xstring list * xstring list * xstring
    1.17 +    -> string list * (string * sort) list * sort
    1.18    val type_name: string -> string
    1.19  
    1.20    (*subclasses*)
    1.21 @@ -419,6 +421,15 @@
    1.22    |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
    1.23    |> Option.map (fst o fst);
    1.24  
    1.25 +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
    1.26 +  let
    1.27 +    val all_arities = map (fn raw_tyco => Sign.read_arity thy
    1.28 +      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    1.29 +    val tycos = map #1 all_arities;
    1.30 +    val (_, sorts, sort) = hd all_arities;
    1.31 +    val vs = Name.names Name.context Name.aT sorts;
    1.32 +  in (tycos, vs, sort) end;
    1.33 +
    1.34  
    1.35  (* syntax *)
    1.36  
    1.37 @@ -578,15 +589,17 @@
    1.38  
    1.39  (* simplified instantiation interface with no class parameter *)
    1.40  
    1.41 -fun instance_arity_cmd arities thy =
    1.42 +fun instance_arity_cmd raw_arities thy =
    1.43    let
    1.44 +    val (tycos, vs, sort) = read_multi_arity thy raw_arities;
    1.45 +    val sorts = map snd vs;
    1.46 +    val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    1.47      fun after_qed results = ProofContext.theory
    1.48        ((fold o fold) AxClass.add_arity results);
    1.49    in
    1.50      thy
    1.51      |> ProofContext.init
    1.52 -    |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
    1.53 -        o Logic.mk_arities o Sign.read_arity thy) arities)
    1.54 +    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
    1.55    end;
    1.56  
    1.57  

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

     3.1 --- a/src/Pure/Isar/theory_target.ML	Mon Jun 29 16:17:56 2009 +0200
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Jun 29 16:17:57 2009 +0200
     3.3 @@ -330,15 +330,6 @@
     3.4         else I)}
     3.5  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
     3.6  
     3.7 -fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
     3.8 -  let
     3.9 -    val all_arities = map (fn raw_tyco => Sign.read_arity thy
    3.10 -      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    3.11 -    val tycos = map #1 all_arities;
    3.12 -    val (_, sorts, sort) = hd all_arities;
    3.13 -    val vs = Name.names Name.context Name.aT sorts;
    3.14 -  in (tycos, vs, sort) end;
    3.15 -
    3.16  fun gen_overloading prep_const raw_ops thy =
    3.17    let
    3.18      val ctxt = ProofContext.init thy;
    3.19 @@ -356,7 +347,7 @@
    3.20  
    3.21  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
    3.22  fun instantiation_cmd raw_arities thy =
    3.23 -  instantiation (read_multi_arity thy raw_arities) thy;
    3.24 +  instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
    3.25  
    3.26  val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
    3.27  val overloading_cmd = gen_overloading Syntax.read_term;