tuned class user space type system code

--- a/src/Pure/Isar/class_target.ML	Sun May 24 15:02:22 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Sun May 24 15:02:22 2009 +0200
@@ -441,12 +441,11 @@
 fun synchronize_inst_syntax ctxt =
   let
     val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
-    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
-    fun subst (c, ty) = case inst_tyco_of (c, ty)
-         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
-             of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
-              | NONE => NONE)
-          | NONE => NONE;
+
+    val lookup_inst_param = AxClass.lookup_inst_param (Sign.consts_of (ProofContext.theory_of ctxt)) params;
+    fun subst (c, ty) = case lookup_inst_param (c, ty)
+     of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
+      | NONE => NONE;
     val unchecks =
       map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   in
@@ -494,38 +493,35 @@
 fun init_instantiation (tycos, vs, sort) thy =
   let
     val _ = if null tycos then error "At least one arity must be given" else ();
-    val params = these_params thy (filter (can (AxClass.get_info thy)) sort);
+    val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
     fun get_param tyco (param, (_, (c, ty))) =
       if can (AxClass.param_of_inst thy) (c, tyco)
       then NONE else SOME ((c, tyco),
         (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
-    val inst_params = map_product get_param tycos params |> map_filter I;
+    val params = map_product get_param tycos class_params |> map_filter I;
     val primary_constraints = map (apsnd
-      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
+      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy
       |> fold (fn tyco => Sorts.add_arities pp
             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)
-      (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
+      (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
     fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
      of NONE => NONE
       | SOME ts' => SOME (ts', ctxt);
-    val inst_tyco_of = AxClass.inst_tyco_of consts;
+    val lookup_inst_param = AxClass.lookup_inst_param consts params;
     val typ_instance = Type.typ_instance (Sign.tsig_of thy);
-    fun improve (c, ty) = case inst_tyco_of (c, ty)
-     of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
-         of SOME (_, ty') => if typ_instance (ty', ty)
-              then SOME (ty, ty') else NONE
-          | NONE => NONE)
+    fun improve (c, ty) = case lookup_inst_param (c, ty)
+     of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
       | NONE => NONE;
   in
     thy
     |> ProofContext.init
-    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
+    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
     |> fold (Variable.declare_typ o TFree) vs
-    |> fold (Variable.declare_names o Free o snd) inst_params
+    |> fold (Variable.declare_names o Free o snd) params
     |> (Overloading.map_improvable_syntax o apfst)
          (K ((primary_constraints, []), (((improve, K NONE), false), [])))
     |> Overloading.add_improvable_syntax

--- 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