# HG changeset patch
# User haftmann
# Date 1388997078 -3600
# Node ID 88cf06038e37dc93c43dbb4ad1bf1caeea587e2c
# Parent  f2ec2829247960143f4fa5d68817de14110d6a0e
uniform orientation of instances as (type constructor, type class)

diff -r f2ec28292479 -r 88cf06038e37 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Jan 05 18:59:29 2014 +0100
+++ b/src/Pure/axclass.ML	Mon Jan 06 09:31:18 2014 +0100
@@ -11,7 +11,7 @@
   val get_info: theory -> class -> info
   val class_of_param: theory -> string -> class option
   val instance_name: string * class -> string
-  val thynames_of_arity: theory -> class * string -> string list
+  val thynames_of_arity: theory -> string * class -> string list
   val param_of_inst: theory -> string * string -> string
   val inst_of_param: theory -> string -> (string * string) option
   val unoverload: theory -> thm -> thm
@@ -216,7 +216,7 @@
   | NONE => error ("Unproven type arity " ^
       Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
 
-fun thynames_of_arity thy (c, a) =
+fun thynames_of_arity thy (a, c) =
   Symtab.lookup_list (proven_arities_of thy) a
   |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
   |> rev;
diff -r f2ec28292479 -r 88cf06038e37 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Jan 05 18:59:29 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Jan 06 09:31:18 2014 +0100
@@ -269,7 +269,7 @@
 local
   fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
   fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
-  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst
+  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy (swap inst)
    of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
     | thyname :: _ => thyname;
   fun thyname_of_const thy c = case Axclass.class_of_param thy c