src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Sun May 24 15:02:22 2009 +0200
+++ b/src/Pure/axclass.ML	Sun May 24 15:02:22 2009 +0200
@@ -26,7 +26,6 @@
   val axiomatize_arity: arity -> theory -> theory
   val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
   val instance_name: string * class -> string
-  val inst_tyco_of: Consts.T -> string * typ -> string option
   val declare_overloaded: string * typ -> theory -> term * theory
   val define_overloaded: binding -> string * term -> theory -> thm * theory
   val unoverload: theory -> thm -> thm
@@ -34,6 +33,7 @@
   val unoverload_conv: theory -> conv
   val overload_conv: theory -> conv
   val unoverload_const: theory -> string * typ -> string
+  val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
   val param_of_inst: theory -> string * string -> string
   val inst_of_param: theory -> string -> (string * string) option
   val arity_property: theory -> class * string -> string -> string list
@@ -249,8 +249,7 @@
 fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
   (get_inst_params thy) [];
 
-fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
-val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
+fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
 
 fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
 fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
@@ -258,9 +257,13 @@
 fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
 fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
 
+fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
+ of SOME tyco => AList.lookup (op =) params (c, tyco)
+  | NONE => NONE;
+
 fun unoverload_const thy (c_ty as (c, _)) =
   case class_of_param thy c
-   of SOME class => (case inst_tyco_of' thy c_ty
+   of SOME class => (case get_inst_tyco (Sign.consts_of thy) c_ty
        of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
         | NONE => c)
     | NONE => c;
@@ -289,15 +292,17 @@
 
 (* declaration and definition of instances of overloaded constants *)
 
+fun inst_tyco_of thy (c, T) = case get_inst_tyco (Sign.consts_of thy) (c, T)
+ of SOME tyco => tyco
+  | NONE => error ("Illegal type for instantiation of class parameter: "
+      ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
+
 fun declare_overloaded (c, T) thy =
   let
     val class = case class_of_param thy c
      of SOME class => class
       | NONE => error ("Not a class parameter: " ^ quote c);
-    val tyco = case inst_tyco_of' thy (c, T)
-     of SOME tyco => tyco
-      | NONE => error ("Illegal type for instantiation of class parameter: "
-        ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
+    val tyco = inst_tyco_of thy (c, T);
     val name_inst = instance_name (tyco, class) ^ "_inst";
     val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
     val T' = Type.strip_sorts T;
@@ -319,7 +324,7 @@
 fun define_overloaded b (c, t) thy =
   let
     val T = Term.fastype_of t;
-    val SOME tyco = inst_tyco_of' thy (c, T);
+    val tyco = inst_tyco_of thy (c, T);
     val (c', eq) = get_inst_param thy (c, tyco);
     val prop = Logic.mk_equals (Const (c', T), t);
     val b' = Thm.def_binding_optional