1.1 --- a/src/Pure/Isar/class_target.ML	Sun May 24 15:02:22 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun May 24 15:02:22 2009 +0200
     1.3 @@ -441,12 +441,11 @@
     1.4  fun synchronize_inst_syntax ctxt =
     1.5    let
     1.6      val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
     1.7 -    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
     1.8 -    fun subst (c, ty) = case inst_tyco_of (c, ty)
     1.9 -         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.10 -             of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    1.11 -              | NONE => NONE)
    1.12 -          | NONE => NONE;
    1.13 +
    1.14 +    val lookup_inst_param = AxClass.lookup_inst_param (Sign.consts_of (ProofContext.theory_of ctxt)) params;
    1.15 +    fun subst (c, ty) = case lookup_inst_param (c, ty)
    1.16 +     of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    1.17 +      | NONE => NONE;
    1.18      val unchecks =
    1.19        map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
    1.20    in
    1.21 @@ -494,38 +493,35 @@
    1.22  fun init_instantiation (tycos, vs, sort) thy =
    1.23    let
    1.24      val _ = if null tycos then error "At least one arity must be given" else ();
    1.25 -    val params = these_params thy (filter (can (AxClass.get_info thy)) sort);
    1.26 +    val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
    1.27      fun get_param tyco (param, (_, (c, ty))) =
    1.28        if can (AxClass.param_of_inst thy) (c, tyco)
    1.29        then NONE else SOME ((c, tyco),
    1.30          (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
    1.31 -    val inst_params = map_product get_param tycos params |> map_filter I;
    1.32 +    val params = map_product get_param tycos class_params |> map_filter I;
    1.33      val primary_constraints = map (apsnd
    1.34 -      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
    1.35 +      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
    1.36      val pp = Syntax.pp_global thy;
    1.37      val algebra = Sign.classes_of thy
    1.38        |> fold (fn tyco => Sorts.add_arities pp
    1.39              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    1.40      val consts = Sign.consts_of thy;
    1.41      val improve_constraints = AList.lookup (op =)
    1.42 -      (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
    1.43 +      (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
    1.44      fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
    1.45       of NONE => NONE
    1.46        | SOME ts' => SOME (ts', ctxt);
    1.47 -    val inst_tyco_of = AxClass.inst_tyco_of consts;
    1.48 +    val lookup_inst_param = AxClass.lookup_inst_param consts params;
    1.49      val typ_instance = Type.typ_instance (Sign.tsig_of thy);
    1.50 -    fun improve (c, ty) = case inst_tyco_of (c, ty)
    1.51 -     of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
    1.52 -         of SOME (_, ty') => if typ_instance (ty', ty)
    1.53 -              then SOME (ty, ty') else NONE
    1.54 -          | NONE => NONE)
    1.55 +    fun improve (c, ty) = case lookup_inst_param (c, ty)
    1.56 +     of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
    1.57        | NONE => NONE;
    1.58    in
    1.59      thy
    1.60      |> ProofContext.init
    1.61 -    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
    1.62 +    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    1.63      |> fold (Variable.declare_typ o TFree) vs
    1.64 -    |> fold (Variable.declare_names o Free o snd) inst_params
    1.65 +    |> fold (Variable.declare_names o Free o snd) params
    1.66      |> (Overloading.map_improvable_syntax o apfst)
    1.67           (K ((primary_constraints, []), (((improve, K NONE), false), [])))
    1.68      |> Overloading.add_improvable_syntax

     2.1 --- a/src/Pure/axclass.ML	Sun May 24 15:02:22 2009 +0200
     2.2 +++ b/src/Pure/axclass.ML	Sun May 24 15:02:22 2009 +0200
     2.3 @@ -26,7 +26,6 @@
     2.4    val axiomatize_arity: arity -> theory -> theory
     2.5    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
     2.6    val instance_name: string * class -> string
     2.7 -  val inst_tyco_of: Consts.T -> string * typ -> string option
     2.8    val declare_overloaded: string * typ -> theory -> term * theory
     2.9    val define_overloaded: binding -> string * term -> theory -> thm * theory
    2.10    val unoverload: theory -> thm -> thm
    2.11 @@ -34,6 +33,7 @@
    2.12    val unoverload_conv: theory -> conv
    2.13    val overload_conv: theory -> conv
    2.14    val unoverload_const: theory -> string * typ -> string
    2.15 +  val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
    2.16    val param_of_inst: theory -> string * string -> string
    2.17    val inst_of_param: theory -> string -> (string * string) option
    2.18    val arity_property: theory -> class * string -> string -> string list
    2.19 @@ -249,8 +249,7 @@
    2.20  fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    2.21    (get_inst_params thy) [];
    2.22  
    2.23 -fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
    2.24 -val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
    2.25 +fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
    2.26  
    2.27  fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    2.28  fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    2.29 @@ -258,9 +257,13 @@
    2.30  fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
    2.31  fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    2.32  
    2.33 +fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
    2.34 + of SOME tyco => AList.lookup (op =) params (c, tyco)
    2.35 +  | NONE => NONE;
    2.36 +
    2.37  fun unoverload_const thy (c_ty as (c, _)) =
    2.38    case class_of_param thy c
    2.39 -   of SOME class => (case inst_tyco_of' thy c_ty
    2.40 +   of SOME class => (case get_inst_tyco (Sign.consts_of thy) c_ty
    2.41         of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
    2.42          | NONE => c)
    2.43      | NONE => c;
    2.44 @@ -289,15 +292,17 @@
    2.45  
    2.46  (* declaration and definition of instances of overloaded constants *)
    2.47  
    2.48 +fun inst_tyco_of thy (c, T) = case get_inst_tyco (Sign.consts_of thy) (c, T)
    2.49 + of SOME tyco => tyco
    2.50 +  | NONE => error ("Illegal type for instantiation of class parameter: "
    2.51 +      ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
    2.52 +
    2.53  fun declare_overloaded (c, T) thy =
    2.54    let
    2.55      val class = case class_of_param thy c
    2.56       of SOME class => class
    2.57        | NONE => error ("Not a class parameter: " ^ quote c);
    2.58 -    val tyco = case inst_tyco_of' thy (c, T)
    2.59 -     of SOME tyco => tyco
    2.60 -      | NONE => error ("Illegal type for instantiation of class parameter: "
    2.61 -        ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
    2.62 +    val tyco = inst_tyco_of thy (c, T);
    2.63      val name_inst = instance_name (tyco, class) ^ "_inst";
    2.64      val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
    2.65      val T' = Type.strip_sorts T;
    2.66 @@ -319,7 +324,7 @@
    2.67  fun define_overloaded b (c, t) thy =
    2.68    let
    2.69      val T = Term.fastype_of t;
    2.70 -    val SOME tyco = inst_tyco_of' thy (c, T);
    2.71 +    val tyco = inst_tyco_of thy (c, T);
    2.72      val (c', eq) = get_inst_param thy (c, tyco);
    2.73      val prop = Logic.mk_equals (Const (c', T), t);
    2.74      val b' = Thm.def_binding_optional