1.1 --- a/src/Pure/axclass.ML	Sun Jan 05 18:59:29 2014 +0100
     1.2 +++ b/src/Pure/axclass.ML	Mon Jan 06 09:31:18 2014 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    val get_info: theory -> class -> info
     1.5    val class_of_param: theory -> string -> class option
     1.6    val instance_name: string * class -> string
     1.7 -  val thynames_of_arity: theory -> class * string -> string list
     1.8 +  val thynames_of_arity: theory -> string * class -> string list
     1.9    val param_of_inst: theory -> string * string -> string
    1.10    val inst_of_param: theory -> string -> (string * string) option
    1.11    val unoverload: theory -> thm -> thm
    1.12 @@ -216,7 +216,7 @@
    1.13    | NONE => error ("Unproven type arity " ^
    1.14        Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
    1.15  
    1.16 -fun thynames_of_arity thy (c, a) =
    1.17 +fun thynames_of_arity thy (a, c) =
    1.18    Symtab.lookup_list (proven_arities_of thy) a
    1.19    |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
    1.20    |> rev;

     2.1 --- a/src/Tools/Code/code_thingol.ML	Sun Jan 05 18:59:29 2014 +0100
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Jan 06 09:31:18 2014 +0100
     2.3 @@ -269,7 +269,7 @@
     2.4  local
     2.5    fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
     2.6    fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
     2.7 -  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst
     2.8 +  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy (swap inst)
     2.9     of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
    2.10      | thyname :: _ => thyname;
    2.11    fun thyname_of_const thy c = case Axclass.class_of_param thy c