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