coherent binding policy with primitive target operations

--- a/src/Pure/Isar/class_target.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 19:17:58 2009 +0100
@@ -43,8 +43,8 @@
   val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
     -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
   val conclude_instantiation: local_theory -> local_theory
-  val instantiation_param: local_theory -> string -> string option
-  val confirm_declaration: string -> local_theory -> local_theory
+  val instantiation_param: local_theory -> binding -> string option
+  val confirm_declaration: binding -> local_theory -> local_theory
   val pretty_instantiation: local_theory -> Pretty.T
   val type_name: string -> string
 
@@ -430,8 +430,8 @@
 
 val instantiation_params = #params o get_instantiation;
 
-fun instantiation_param lthy v = instantiation_params lthy
-  |> find_first (fn (_, (v', _)) => v = v')
+fun instantiation_param lthy b = instantiation_params lthy
+  |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
   |> Option.map (fst o fst);
 
 
@@ -530,8 +530,8 @@
     |> synchronize_inst_syntax
   end;
 
-fun confirm_declaration c = (map_instantiation o apsnd)
-  (filter_out (fn (_, (c', _)) => c' = c))
+fun confirm_declaration b = (map_instantiation o apsnd)
+  (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
   #> LocalTheory.target synchronize_inst_syntax
 
 fun gen_instantiation_instance do_proof after_qed lthy =

--- a/src/Pure/Isar/overloading.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/Pure/Isar/overloading.ML	Fri Mar 13 19:17:58 2009 +0100
@@ -9,9 +9,9 @@
   val init: (string * (string * typ) * bool) list -> theory -> local_theory
   val conclude: local_theory -> local_theory
   val declare: string * typ -> theory -> term * theory
-  val confirm: string -> local_theory -> local_theory
-  val define: bool -> string -> string * term -> theory -> thm * theory
-  val operation: Proof.context -> string -> (string * bool) option
+  val confirm: binding -> local_theory -> local_theory
+  val define: bool -> binding -> string * term -> theory -> thm * theory
+  val operation: Proof.context -> binding -> (string * bool) option
   val pretty: Proof.context -> Pretty.T
   
   type improvable_syntax
@@ -123,18 +123,19 @@
 val get_overloading = OverloadingData.get o LocalTheory.target_of;
 val map_overloading = LocalTheory.target o OverloadingData.map;
 
-fun operation lthy v = get_overloading lthy
-  |> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
+fun operation lthy b = get_overloading lthy
+  |> get_first (fn ((c, _), (v, checked)) =>
+      if Binding.name_of b = v then SOME (c, checked) else NONE);
 
-fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
+fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));
 
 
 (* overloaded declarations and definitions *)
 
 fun declare c_ty = pair (Const c_ty);
 
-fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
-  Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked b (c, t) = Thm.add_def (not checked) true
+  (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
 
 
 (* target *)

--- a/src/Pure/Isar/theory_target.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Mar 13 19:17:58 2009 +0100
@@ -188,10 +188,7 @@
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (fn thy => thy
-          |> Sign.no_base_names
-          |> Sign.add_abbrev PrintMode.internal tags legacy_arg
-          ||> Sign.restore_naming thy)
+        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
         (ProofContext.add_abbrev PrintMode.internal tags arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           similar_body ?
@@ -203,23 +200,22 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val c = Binding.qualified_name_of b;
     val tags = LocalTheory.group_position_of lthy;
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val declare_const =
-      (case Class_Target.instantiation_param lthy c of
+      (case Class_Target.instantiation_param lthy b of
         SOME c' =>
           if mx3 <> NoSyn then syntax_error c'
           else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
-            ##> Class_Target.confirm_declaration c
+            ##> Class_Target.confirm_declaration b
         | NONE =>
-            (case Overloading.operation lthy c of
+            (case Overloading.operation lthy b of
               SOME (c', _) =>
                 if mx3 <> NoSyn then syntax_error c'
                 else LocalTheory.theory_result (Overloading.declare (c', U))
-                  ##> Overloading.confirm c
+                  ##> Overloading.confirm b
             | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
     val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
@@ -282,17 +278,14 @@
     val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
 
     (*def*)
-    val c = Binding.qualified_name_of b;
-    val define_const =
-      (case Overloading.operation lthy c of
-        SOME (_, checked) =>
-          (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
-      | NONE =>
-          if is_none (Class_Target.instantiation_param lthy c)
-          then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
-          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
     val (global_def, lthy3) = lthy2
-      |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
+      |> LocalTheory.theory_result (case Overloading.operation lthy b of
+          SOME (_, checked) =>
+            Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
+        | NONE =>
+            if is_none (Class_Target.instantiation_param lthy b)
+            then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
+            else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
     val def = LocalDefs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,

--- a/src/Pure/axclass.ML	Fri Mar 13 19:17:57 2009 +0100
+++ b/src/Pure/axclass.ML	Fri Mar 13 19:17:58 2009 +0100
@@ -27,7 +27,7 @@
   val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
   val instance_name: string * class -> string
   val declare_overloaded: string * typ -> theory -> term * theory
-  val define_overloaded: string -> string * term -> theory -> thm * theory
+  val define_overloaded: binding -> string * term -> theory -> thm * theory
   val inst_tyco_of: theory -> string * typ -> string option
   val unoverload: theory -> thm -> thm
   val overload: theory -> thm -> thm
@@ -383,16 +383,17 @@
       #> pair (Const (c, T))))
   end;
 
-fun define_overloaded name (c, t) thy =
+fun define_overloaded b (c, t) thy =
   let
     val T = Term.fastype_of t;
     val SOME 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 name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name;
+    val b' = Thm.def_binding_optional
+      (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b;
   in
     thy
-    |> Thm.add_def false false (Binding.name name', prop)
+    |> Thm.add_def false false (b', prop)
     |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   end;