1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Dec 10 11:24:14 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Dec 10 11:24:15 2007 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4      |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
     1.5      |> Thm.implies_intr asm
     1.6      |> Thm.generalize ([], params) 0
     1.7 -    |> Class.unoverload thy
     1.8 +    |> AxClass.unoverload thy
     1.9      |> Thm.varifyT
    1.10    end;
    1.11  
    1.12 @@ -426,7 +426,7 @@
    1.13      fun add_eq_thms dtco thy =
    1.14        let
    1.15          val thy_ref = Theory.check_thy thy;
    1.16 -        val const = Class.param_of_inst thy ("op =", dtco);
    1.17 +        val const = AxClass.param_of_inst thy ("op =", dtco);
    1.18          val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
    1.19        in
    1.20          Code.add_funcl (const, Susp.delay get_thms) thy

     2.1 --- a/src/Pure/Isar/class.ML	Mon Dec 10 11:24:14 2007 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Mon Dec 10 11:24:15 2007 +0100
     2.3 @@ -36,20 +36,9 @@
     2.4    val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
     2.5    val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
     2.6    val conclude_instantiation: local_theory -> local_theory
     2.7 -
     2.8 -  val overloaded_const: string * typ -> theory -> term * theory
     2.9 -  val overloaded_def: string -> string * term -> theory -> thm * theory
    2.10    val instantiation_param: Proof.context -> string -> string option
    2.11    val confirm_declaration: string -> local_theory -> local_theory
    2.12  
    2.13 -  val unoverload: theory -> thm -> thm
    2.14 -  val overload: theory -> thm -> thm
    2.15 -  val unoverload_conv: theory -> conv
    2.16 -  val overload_conv: theory -> conv
    2.17 -  val unoverload_const: theory -> string * typ -> string
    2.18 -  val param_of_inst: theory -> string * string -> string
    2.19 -  val inst_of_param: theory -> string -> (string * string) option
    2.20 -
    2.21    (*old axclass layer*)
    2.22    val axclass_cmd: bstring * xstring list
    2.23      -> ((bstring * Attrib.src list) * string list) list
    2.24 @@ -152,96 +141,6 @@
    2.25  end; (*local*)
    2.26  
    2.27  
    2.28 -(** basic overloading **)
    2.29 -
    2.30 -(* bookkeeping *)
    2.31 -
    2.32 -structure InstData = TheoryDataFun
    2.33 -(
    2.34 -  type T = (string * thm) Symtab.table Symtab.table * (string * string) Symtab.table;
    2.35 -    (*constant name ~> type constructor ~> (constant name, equation),
    2.36 -        constant name ~> (constant name, type constructor)*)
    2.37 -  val empty = (Symtab.empty, Symtab.empty);
    2.38 -  val copy = I;
    2.39 -  val extend = I;
    2.40 -  fun merge _ ((taba1, tabb1), (taba2, tabb2)) =
    2.41 -    (Symtab.join (K (Symtab.merge (K true))) (taba1, taba2),
    2.42 -      Symtab.merge (K true) (tabb1, tabb2));
    2.43 -);
    2.44 -
    2.45 -val inst_tyco = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
    2.46 -
    2.47 -fun inst thy (c, tyco) =
    2.48 -  (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
    2.49 -
    2.50 -val param_of_inst = fst oo inst;
    2.51 -
    2.52 -fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    2.53 -  (InstData.get thy) [];
    2.54 -
    2.55 -val inst_of_param = Symtab.lookup o snd o InstData.get;
    2.56 -
    2.57 -fun add_inst (c, tyco) inst = (InstData.map o apfst
    2.58 -      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
    2.59 -  #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
    2.60 -
    2.61 -fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    2.62 -fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    2.63 -
    2.64 -fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
    2.65 -fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    2.66 -
    2.67 -fun unoverload_const thy (c_ty as (c, _)) =
    2.68 -  case AxClass.class_of_param thy c
    2.69 -   of SOME class => (case inst_tyco thy c_ty
    2.70 -       of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
    2.71 -        | NONE => c)
    2.72 -    | NONE => c;
    2.73 -
    2.74 -
    2.75 -(* declaration and definition of instances of overloaded constants *)
    2.76 -
    2.77 -fun primitive_note kind (name, thm) =
    2.78 -  PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
    2.79 -  #>> (fn [(_, [thm])] => thm);
    2.80 -
    2.81 -fun overloaded_const (c, ty) thy =
    2.82 -  let
    2.83 -    val SOME class = AxClass.class_of_param thy c;
    2.84 -    val SOME tyco = inst_tyco thy (c, ty);
    2.85 -    val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
    2.86 -    val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
    2.87 -    val ty' = Type.strip_sorts ty;
    2.88 -  in
    2.89 -    thy
    2.90 -    |> Sign.sticky_prefix name_inst
    2.91 -    |> Sign.no_base_names
    2.92 -    |> Sign.declare_const [] (c', ty', NoSyn)
    2.93 -    |-> (fn const' as Const (c'', _) => Thm.add_def false true
    2.94 -          (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
    2.95 -    #>> Thm.varifyT
    2.96 -    #-> (fn thm => add_inst (c, tyco) (c'', thm)
    2.97 -    #> primitive_note Thm.internalK (c', thm)
    2.98 -    #> snd
    2.99 -    #> Sign.restore_naming thy
   2.100 -    #> pair (Const (c, ty))))
   2.101 -  end;
   2.102 -
   2.103 -fun overloaded_def name (c, t) thy =
   2.104 -  let
   2.105 -    val ty = Term.fastype_of t;
   2.106 -    val SOME tyco = inst_tyco thy (c, ty);
   2.107 -    val (c', eq) = inst thy (c, tyco);
   2.108 -    val prop = Logic.mk_equals (Const (c', ty), t);
   2.109 -    val name' = Thm.def_name_optional
   2.110 -      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   2.111 -  in
   2.112 -    thy
   2.113 -    |> Thm.add_def false false (name', prop)
   2.114 -    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   2.115 -  end;
   2.116 -
   2.117 -
   2.118  (** class data **)
   2.119  
   2.120  datatype class_data = ClassData of {
   2.121 @@ -859,7 +758,8 @@
   2.122  
   2.123  (* syntax *)
   2.124  
   2.125 -fun subst_param thy params = map_aterms (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
   2.126 +fun subst_param thy params = map_aterms (fn t as Const (c, ty) =>
   2.127 +    (case AxClass.inst_tyco_of thy (c, ty)
   2.128       of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   2.129           of SOME v_ty => Free v_ty
   2.130            | NONE => t)
   2.131 @@ -878,7 +778,7 @@
   2.132      val tsig = ProofContext.tsig_of lthy;
   2.133      val thy = ProofContext.theory_of lthy;
   2.134  
   2.135 -    fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
   2.136 +    fun check_improve (Const (c, ty)) = (case AxClass.inst_tyco_of thy (c, ty)
   2.137           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   2.138               of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty')))
   2.139                | NONE => I)
   2.140 @@ -925,8 +825,8 @@
   2.141      fun type_name "*" = "prod"
   2.142        | type_name "+" = "sum"
   2.143        | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   2.144 -    fun get_param tyco (param, (c, ty)) = if can (inst thy) (c, tyco)
   2.145 -      then NONE else SOME ((unoverload_const thy (c, ty), tyco),
   2.146 +    fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
   2.147 +      then NONE else SOME ((AxClass.unoverload_const thy (c, ty), tyco),
   2.148          (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
   2.149      val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
   2.150    in
   2.151 @@ -965,40 +865,10 @@
   2.152      val { arities, params } = the_instantiation lthy;
   2.153      val (tycos, sorts, sort) = arities;
   2.154      val thy = ProofContext.theory_of lthy;
   2.155 -    (*val _ = map (fn (tyco, sorts, sort) =>
   2.156 -      if Sign.of_sort thy
   2.157 +    val _ = map (fn tyco => if Sign.of_sort thy
   2.158          (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
   2.159        then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   2.160 -        arities; FIXME activate when old instance command is gone*)
   2.161 -    val params_of = maps (these o try (#params o AxClass.get_info thy))
   2.162 -      o Sign.complete_sort thy;
   2.163 -    val missing_params = tycos
   2.164 -      |> maps (fn tyco => params_of sort |> map (rpair tyco))
   2.165 -      |> filter_out (can (inst thy) o apfst fst);
   2.166 -    fun declare_missing ((c, ty0), tyco) thy =
   2.167 -    (*fun declare_missing ((c, tyco), (_, ty)) thy =*)
   2.168 -      let
   2.169 -        val SOME class = AxClass.class_of_param thy c;
   2.170 -        val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
   2.171 -        val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
   2.172 -        val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
   2.173 -        val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
   2.174 -      in
   2.175 -        thy
   2.176 -        |> Sign.sticky_prefix name_inst
   2.177 -        |> Sign.no_base_names
   2.178 -        |> Sign.declare_const [] (c', ty, NoSyn)
   2.179 -        |-> (fn const' as Const (c'', _) => Thm.add_def false true
   2.180 -              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
   2.181 -        #>> Thm.varifyT
   2.182 -        #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
   2.183 -        #> primitive_note Thm.internalK (c', thm)
   2.184 -        #> snd
   2.185 -        #> Sign.restore_naming thy))
   2.186 -      end;
   2.187 -  in
   2.188 -    lthy
   2.189 -    |> LocalTheory.theory (fold declare_missing missing_params)
   2.190 -  end;
   2.191 +        tycos;
   2.192 +  in lthy end;
   2.193  
   2.194  end;

     3.1 --- a/src/Pure/Isar/code.ML	Mon Dec 10 11:24:14 2007 +0100
     3.2 +++ b/src/Pure/Isar/code.ML	Mon Dec 10 11:24:15 2007 +0100
     3.3 @@ -518,7 +518,7 @@
     3.4            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
     3.5        in map (Thm.instantiate (instT, [])) thms' end;
     3.6  
     3.7 -fun const_of_func thy = Class.unoverload_const thy o CodeUnit.head_func;
     3.8 +fun const_of_func thy = AxClass.unoverload_const thy o CodeUnit.head_func;
     3.9  
    3.10  fun certify_const thy const thms =
    3.11    let
    3.12 @@ -547,7 +547,7 @@
    3.13      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
    3.14      val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
    3.15      val funcs = classparams
    3.16 -      |> map_filter (fn c => try (Class.param_of_inst thy) (c, tyco))
    3.17 +      |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
    3.18        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
    3.19        |> (map o Option.map) (Susp.force o fst o snd)
    3.20        |> maps these
    3.21 @@ -665,7 +665,7 @@
    3.22             ^ CodeUnit.string_of_typ thy ty_decl)
    3.23        end;
    3.24      fun check_typ (c, thm) =
    3.25 -      case Class.inst_of_param thy c
    3.26 +      case AxClass.inst_of_param thy c
    3.27         of SOME (c, tyco) => check_typ_classparam tyco (c, thm)
    3.28          | NONE => check_typ_fun (c, thm);
    3.29    in check_typ (const_of_func thy thm, thm) end;
    3.30 @@ -782,7 +782,7 @@
    3.31  
    3.32  fun add_datatype raw_cs thy =
    3.33    let
    3.34 -    val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
    3.35 +    val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
    3.36      val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
    3.37      val cs' = map fst (snd vs_cos);
    3.38      val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
    3.39 @@ -909,7 +909,7 @@
    3.40    |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
    3.41  (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
    3.42    |> common_typ_funcs
    3.43 -  |> map (Class.unoverload thy);
    3.44 +  |> map (AxClass.unoverload thy);
    3.45  
    3.46  fun preprocess_conv ct =
    3.47    let
    3.48 @@ -919,7 +919,7 @@
    3.49      |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
    3.50      |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
    3.51          ((#inline_procs o the_thmproc o the_exec) thy)
    3.52 -    |> rhs_conv (Class.unoverload_conv thy)
    3.53 +    |> rhs_conv (AxClass.unoverload_conv thy)
    3.54    end;
    3.55  
    3.56  fun preprocess_term thy = term_of_conv thy preprocess_conv;
    3.57 @@ -929,7 +929,7 @@
    3.58      val thy = Thm.theory_of_cterm ct;
    3.59    in
    3.60      ct
    3.61 -    |> Class.overload_conv thy
    3.62 +    |> AxClass.overload_conv thy
    3.63      |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
    3.64    end;
    3.65  
    3.66 @@ -937,7 +937,7 @@
    3.67  
    3.68  end; (*local*)
    3.69  
    3.70 -fun default_typ_proto thy c = case Class.inst_of_param thy c
    3.71 +fun default_typ_proto thy c = case AxClass.inst_of_param thy c
    3.72   of SOME (c, tyco) => classparam_weakest_typ thy ((the o AxClass.class_of_param thy) c)
    3.73        (c, tyco) |> SOME
    3.74    | NONE => (case AxClass.class_of_param thy c
    3.75 @@ -968,7 +968,7 @@
    3.76  fun default_typ thy c = case default_typ_proto thy c
    3.77   of SOME ty => ty
    3.78    | NONE => (case get_funcs thy c
    3.79 -     of thm :: _ => snd (CodeUnit.head_func (Class.unoverload thy thm))
    3.80 +     of thm :: _ => snd (CodeUnit.head_func (AxClass.unoverload thy thm))
    3.81        | [] => Sign.the_const_type thy c);
    3.82  
    3.83  end; (*local*)

     4.1 --- a/src/Pure/Isar/code_unit.ML	Mon Dec 10 11:24:14 2007 +0100
     4.2 +++ b/src/Pure/Isar/code_unit.ML	Mon Dec 10 11:24:15 2007 +0100
     4.3 @@ -60,7 +60,7 @@
     4.4  fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
     4.5  
     4.6  fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
     4.7 -fun string_of_const thy c = case Class.inst_of_param thy c
     4.8 +fun string_of_const thy c = case AxClass.inst_of_param thy c
     4.9   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
    4.10    | NONE => Sign.extern_const thy c;
    4.11  
    4.12 @@ -76,7 +76,7 @@
    4.13      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    4.14    end;
    4.15  
    4.16 -fun read_const thy = Class.unoverload_const thy o read_bare_const thy;
    4.17 +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
    4.18  
    4.19  local
    4.20  

     5.1 --- a/src/Pure/Isar/theory_target.ML	Mon Dec 10 11:24:14 2007 +0100
     5.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Dec 10 11:24:15 2007 +0100
     5.3 @@ -203,7 +203,7 @@
     5.4      fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
     5.5      val declare_const = case Class.instantiation_param lthy c
     5.6         of SOME c' => if mx3 <> NoSyn then syntax_error c'
     5.7 -          else LocalTheory.theory_result (Class.overloaded_const (c', U))
     5.8 +          else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
     5.9              ##> Class.confirm_declaration c
    5.10          | NONE => (case Overloading.operation lthy c
    5.11             of SOME (c', _) => if mx3 <> NoSyn then syntax_error c'
    5.12 @@ -276,7 +276,7 @@
    5.13            (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    5.14        | NONE => if is_none (Class.instantiation_param lthy c)
    5.15            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    5.16 -          else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    5.17 +          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs));
    5.18      val (global_def, lthy3) = lthy2
    5.19        |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
    5.20      val def = LocalDefs.trans_terms lthy3

     6.1 --- a/src/Pure/axclass.ML	Mon Dec 10 11:24:14 2007 +0100
     6.2 +++ b/src/Pure/axclass.ML	Mon Dec 10 11:24:15 2007 +0100
     6.3 @@ -27,6 +27,16 @@
     6.4    val axiomatize_arity: arity -> theory -> theory
     6.5    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
     6.6    val instance_name: string * class -> string
     6.7 +  val declare_overloaded: string * typ -> theory -> term * theory
     6.8 +  val define_overloaded: string -> string * term -> theory -> thm * theory
     6.9 +  val inst_tyco_of: theory -> string * typ -> string option
    6.10 +  val unoverload: theory -> thm -> thm
    6.11 +  val overload: theory -> thm -> thm
    6.12 +  val unoverload_conv: theory -> conv
    6.13 +  val overload_conv: theory -> conv
    6.14 +  val unoverload_const: theory -> string * typ -> string
    6.15 +  val param_of_inst: theory -> string * string -> string
    6.16 +  val inst_of_param: theory -> string -> (string * string) option
    6.17    type cache
    6.18    val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
    6.19    val cache: cache
    6.20 @@ -88,23 +98,36 @@
    6.21    Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
    6.22  
    6.23  
    6.24 +(* instance parameters *)
    6.25 +
    6.26 +type inst_params =
    6.27 +  (string * thm) Symtab.table Symtab.table
    6.28 +    (*constant name ~> type constructor ~> (constant name, equation)*)
    6.29 +  * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
    6.30 +
    6.31 +fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
    6.32 +  (Symtab.join  (K (Symtab.merge (K true))) (const_param1, const_param2),
    6.33 +    Symtab.merge (K true) (param_const1, param_const2));
    6.34 +
    6.35 +
    6.36  (* setup data *)
    6.37  
    6.38  structure AxClassData = TheoryDataFun
    6.39  (
    6.40 -  type T = axclasses * instances;
    6.41 -  val empty = ((Symtab.empty, []), ([], Symtab.empty));
    6.42 +  type T = axclasses * (instances * inst_params);
    6.43 +  val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
    6.44    val copy = I;
    6.45    val extend = I;
    6.46 -  fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
    6.47 -    (merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2)));
    6.48 +  fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
    6.49 +    (merge_axclasses pp (axclasses1, axclasses2),
    6.50 +      (merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)));
    6.51  );
    6.52  
    6.53  
    6.54  (* maintain axclasses *)
    6.55  
    6.56  val get_axclasses = #1 o AxClassData.get;
    6.57 -fun map_axclasses f = AxClassData.map (apfst f);
    6.58 +val map_axclasses = AxClassData.map o apfst;
    6.59  
    6.60  val lookup_def = Symtab.lookup o #1 o get_axclasses;
    6.61  
    6.62 @@ -135,8 +158,8 @@
    6.63  
    6.64  fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a;
    6.65  
    6.66 -val get_instances = #2 o AxClassData.get;
    6.67 -fun map_instances f = AxClassData.map (apsnd f);
    6.68 +val get_instances = #1 o #2 o AxClassData.get;
    6.69 +val map_instances = AxClassData.map o apsnd o apfst;
    6.70  
    6.71  
    6.72  fun the_classrel thy (c1, c2) =
    6.73 @@ -159,6 +182,39 @@
    6.74    (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
    6.75  
    6.76  
    6.77 +(* maintain instance parameters *)
    6.78 +
    6.79 +val get_inst_params = #2 o #2 o AxClassData.get;
    6.80 +val map_inst_params = AxClassData.map o apsnd o apsnd;
    6.81 +
    6.82 +fun get_inst_param thy (c, tyco) =
    6.83 +  (the o Symtab.lookup ((the o Symtab.lookup (fst (get_inst_params thy))) c)) tyco;
    6.84 +
    6.85 +fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
    6.86 +      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
    6.87 +  #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
    6.88 +
    6.89 +val inst_of_param = Symtab.lookup o snd o get_inst_params;
    6.90 +val param_of_inst = fst oo get_inst_param;
    6.91 +
    6.92 +fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    6.93 +  (get_inst_params thy) [];
    6.94 +
    6.95 +val inst_tyco_of = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
    6.96 +
    6.97 +fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    6.98 +fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    6.99 +
   6.100 +fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
   6.101 +fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   6.102 +
   6.103 +fun unoverload_const thy (c_ty as (c, _)) =
   6.104 +  case class_of_param thy c
   6.105 +   of SOME class => (case inst_tyco_of thy c_ty
   6.106 +       of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   6.107 +        | NONE => c)
   6.108 +    | NONE => c;
   6.109 +
   6.110  
   6.111  (** instances **)
   6.112  
   6.113 @@ -200,10 +256,35 @@
   6.114      val prop = Thm.plain_prop_of (Thm.transfer thy th);
   6.115      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   6.116      val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
   6.117 +    (*FIXME turn this into a mere check as soon as "attach" has disappeared*)
   6.118 +    val missing_params = Sign.complete_sort thy [c]
   6.119 +      |> maps (these o Option.map (fn AxClass { params, ... } => params) o lookup_def thy)
   6.120 +      |> filter_out (fn (p, _) => can (get_inst_param thy) (p, t));
   6.121 +    fun declare_missing (p, T0) thy =
   6.122 +      let
   6.123 +        val name_inst = instance_name (t, c) ^ "_inst";
   6.124 +        val p' = NameSpace.base p ^ "_" ^ NameSpace.base t;
   6.125 +        val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy t) []);
   6.126 +        val T = map_atyps (fn _ => Type (t, map TFree vs)) T0;
   6.127 +      in
   6.128 +        thy
   6.129 +        |> Sign.sticky_prefix name_inst
   6.130 +        |> Sign.no_base_names
   6.131 +        |> Sign.declare_const [] (p', T, NoSyn)
   6.132 +        |-> (fn const' as Const (p'', _) => Thm.add_def false true
   6.133 +              (Thm.def_name p', Logic.mk_equals (const', Const (p, T)))
   6.134 +        #>> Thm.varifyT
   6.135 +        #-> (fn thm => add_inst_param (p, t) (p'', Thm.symmetric thm)
   6.136 +        #> PureThy.note Thm.internalK (p', thm)
   6.137 +        #> snd
   6.138 +        #> Sign.restore_naming thy))
   6.139 +      end;
   6.140 +
   6.141    in
   6.142      thy
   6.143      |> Sign.primitive_arity (t, Ss, [c])
   6.144      |> put_arity ((t, Ss, c), Drule.unconstrainTs th)
   6.145 +    |> fold declare_missing missing_params
   6.146    end;
   6.147  
   6.148  
   6.149 @@ -240,6 +321,47 @@
   6.150    end;
   6.151  
   6.152  
   6.153 +(* instance parameters and overloaded definitions *)
   6.154 +
   6.155 +(* declaration and definition of instances of overloaded constants *)
   6.156 +
   6.157 +fun declare_overloaded (c, T) thy =
   6.158 +  let
   6.159 +    val SOME class = class_of_param thy c;
   6.160 +    val SOME tyco = inst_tyco_of thy (c, T);
   6.161 +    val name_inst = instance_name (tyco, class) ^ "_inst";
   6.162 +    val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
   6.163 +    val T' = Type.strip_sorts T;
   6.164 +  in
   6.165 +    thy
   6.166 +    |> Sign.sticky_prefix name_inst
   6.167 +    |> Sign.no_base_names
   6.168 +    |> Sign.declare_const [] (c', T', NoSyn)
   6.169 +    |-> (fn const' as Const (c'', _) => Thm.add_def false true
   6.170 +          (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
   6.171 +    #>> Thm.varifyT
   6.172 +    #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
   6.173 +    #> PureThy.note Thm.internalK (c', thm)
   6.174 +    #> snd
   6.175 +    #> Sign.restore_naming thy
   6.176 +    #> pair (Const (c, T))))
   6.177 +  end;
   6.178 +
   6.179 +fun define_overloaded name (c, t) thy =
   6.180 +  let
   6.181 +    val T = Term.fastype_of t;
   6.182 +    val SOME tyco = inst_tyco_of thy (c, T);
   6.183 +    val (c', eq) = get_inst_param thy (c, tyco);
   6.184 +    val prop = Logic.mk_equals (Const (c', T), t);
   6.185 +    val name' = Thm.def_name_optional
   6.186 +      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   6.187 +  in
   6.188 +    thy
   6.189 +    |> Thm.add_def false false (name', prop)
   6.190 +    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   6.191 +  end;
   6.192 +
   6.193 +
   6.194  
   6.195  (** class definitions **)
   6.196  

     7.1 --- a/src/Tools/code/code_funcgr.ML	Mon Dec 10 11:24:14 2007 +0100
     7.2 +++ b/src/Tools/code/code_funcgr.ML	Mon Dec 10 11:24:15 2007 +0100
     7.3 @@ -157,7 +157,7 @@
     7.4      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     7.5      fun all_classparams tyco class =
     7.6        these (try (#params o AxClass.get_info thy) class)
     7.7 -      |> map (fn (c, _) => Class.param_of_inst thy (c, tyco))
     7.8 +      |> map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
     7.9    in
    7.10      Symtab.empty
    7.11      |> fold (fn (tyco, class) =>
    7.12 @@ -211,7 +211,7 @@
    7.13        |> resort_funcss thy algebra funcgr
    7.14        |> filter_out (can (Graph.get_node funcgr) o fst);
    7.15      fun typ_func c [] = Code.default_typ thy c
    7.16 -      | typ_func c (thms as thm :: _) = case Class.inst_of_param thy c
    7.17 +      | typ_func c (thms as thm :: _) = case AxClass.inst_of_param thy c
    7.18           of SOME (c', tyco) => 
    7.19                let
    7.20                  val (_, ty) = CodeUnit.head_func thm;

     8.1 --- a/src/Tools/code/code_name.ML	Mon Dec 10 11:24:14 2007 +0100
     8.2 +++ b/src/Tools/code/code_name.ML	Mon Dec 10 11:24:15 2007 +0100
     8.3 @@ -216,7 +216,7 @@
     8.4   of SOME dtco => SOME (thyname_of_tyco thy dtco)
     8.5    | NONE => (case AxClass.class_of_param thy c
     8.6       of SOME class => SOME (thyname_of_class thy class)
     8.7 -      | NONE => (case Class.inst_of_param thy c
     8.8 +      | NONE => (case AxClass.inst_of_param thy c
     8.9           of SOME (c, tyco) => SOME (thyname_of_instance thy
    8.10                ((the o AxClass.class_of_param thy) c, tyco))
    8.11            | NONE => NONE));

     9.1 --- a/src/Tools/code/code_package.ML	Mon Dec 10 11:24:14 2007 +0100
     9.2 +++ b/src/Tools/code/code_package.ML	Mon Dec 10 11:24:15 2007 +0100
     9.3 @@ -33,7 +33,7 @@
     9.4        in
     9.5          gr
     9.6          |> Graph.subgraph (member (op =) select) 
     9.7 -        |> Graph.map_nodes ((apsnd o map) (Class.overload thy))
     9.8 +        |> Graph.map_nodes ((apsnd o map) (AxClass.overload thy))
     9.9        end;
    9.10  
    9.11  fun code_thms thy =
    9.12 @@ -162,7 +162,7 @@
    9.13        | SOME thm => let
    9.14            val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;
    9.15            val cs = fold_aterms (fn Const (c, ty) =>
    9.16 -            cons (Class.unoverload_const thy (c, ty)) | _ => I) t [];
    9.17 +            cons (AxClass.unoverload_const thy (c, ty)) | _ => I) t [];
    9.18          in if exists (member (op =) sel_cs) cs
    9.19            andalso forall (member (op =) all_cs) cs
    9.20            then SOME (thmref, thm) else NONE end;

    10.1 --- a/src/Tools/code/code_thingol.ML	Mon Dec 10 11:24:14 2007 +0100
    10.2 +++ b/src/Tools/code/code_thingol.ML	Mon Dec 10 11:24:15 2007 +0100
    10.3 @@ -461,7 +461,7 @@
    10.4      fun exprgen_classparam_inst (c, ty) =
    10.5        let
    10.6          val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
    10.7 -        val thm = Class.unoverload_conv thy (Thm.cterm_of thy c_inst);
    10.8 +        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
    10.9          val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
   10.10            o Logic.dest_equals o Thm.prop_of) thm;
   10.11        in